header {* \isaheader{An intermediate language} *}
theory J1 imports "J0" begin
types
expr1 = "(nat,nat) exp"
J1_prog = "expr1 prog"
locals1 = "val list"
translations
"expr1" <= (type) "(nat, nat) exp"
"J1_prog" <= (type) "expr1 prog"
types
J1state = "(expr1 × locals1) list"
types
J1_thread_action = "(addr,thread_id,(expr1 × locals1) × (expr1 × locals1) list,heap,addr,obs_event option) thread_action"
translations
"J1_thread_action" <= (type) "(nat,nat,(expr1 × val list) × (expr1 × val list) list,heap,nat,obs_event option) thread_action"
primrec max_vars:: "('a,'b) exp => nat"
and max_varss:: "('a,'b) exp list => nat"
where
"max_vars (new C) = 0"
| "max_vars (newA T⌊e⌉) = max_vars e"
| "max_vars (Cast C e) = max_vars e"
| "max_vars (Val v) = 0"
| "max_vars (e «bop» e') = max (max_vars e) (max_vars e')"
| "max_vars (Var V) = 0"
| "max_vars (V:=e) = max_vars e"
| "max_vars (a⌊i⌉) = max (max_vars a) (max_vars i)"
| "max_vars (AAss a i e) = max (max (max_vars a) (max_vars i)) (max_vars e)"
| "max_vars (a•length) = max_vars a"
| "max_vars (e•F{D}) = max_vars e"
| "max_vars (FAss e1 F D e2) = max (max_vars e1) (max_vars e2)"
| "max_vars (e•M(es)) = max (max_vars e) (max_varss es)"
| "max_vars ({V:T=vo; e}) = max_vars e + 1"
| "max_vars (syncV (e') e) = max (max_vars e') (max_vars e + 1)"
| "max_vars (insyncV (a) e) = max_vars e + 1"
| "max_vars (e1;;e2) = max (max_vars e1) (max_vars e2)"
| "max_vars (if (e) e1 else e2) =
max (max_vars e) (max (max_vars e1) (max_vars e2))"
| "max_vars (while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars (throw e) = max_vars e"
| "max_vars (try e1 catch(C V) e2) = max (max_vars e1) (max_vars e2 + 1)"
| "max_varss [] = 0"
| "max_varss (e#es) = max (max_vars e) (max_varss es)"
lemma max_varss_append [simp]:
"max_varss (es @ es') = max (max_varss es) (max_varss es')"
by(induct es, auto)
lemma max_varss_map_Val [simp]: "max_varss (map Val vs) = 0"
by(induct vs) auto
lemma max_vars_inline_call: "max_vars (inline_call e' e) ≤ max_vars e + max_vars e'"
and max_varss_inline_calls: "max_varss (inline_calls e' es) ≤ max_varss es + max_vars e'"
by(induct e and es) auto
definition extNTA2J1 :: "J1_prog => (cname × mname × addr) => ((expr1 × locals1) × (expr1 × locals1) list)"
where
"extNTA2J1 P = (λ(C, M, a). let (D, _, _, body) = method P C M
in (({0:Class D=None; body}, Addr a # replicate (max_vars body) undefined), [(addr a•M([]), [])]))"
lemma extNTA2J1_iff [simp]:
"extNTA2J1 P (C, M, a) = (({0:Class (fst (method P C M))=None; snd (snd (snd (method P C M)))}, Addr a # replicate (max_vars (snd (snd (snd (method P C M))))) undefined), [(addr a•M([]), [])])"
by(simp add: extNTA2J1_def split_beta)
abbreviation extTA2J1 :: "J1_prog => external_thread_action => J1_thread_action"
where "extTA2J1 P ≡ convert_extTA (extNTA2J1 P)"
abbreviation (input) extRet2J1 :: "val + addr => expr1"
where "extRet2J1 ≡ extRet2J"
lemma max_vars_extRet2J1 [simp]:
"max_vars (extRet2J1 va) = 0"
by(cases va) simp_all
inductive red1 :: "J1_prog => expr1 => heap × locals1 => external_thread_action => expr1 => heap × locals1 => bool"
("_ \<turnstile>1 ((1⟨_,/_⟩) -_->/ (1⟨_,/_⟩))" [51,0,0,0,0,0] 81)
and reds1 :: "J1_prog => expr1 list => heap × locals1 => external_thread_action => expr1 list => heap × locals1 => bool"
("_ \<turnstile>1 ((1⟨_,/_⟩) [-_->]/ (1⟨_,/_⟩))" [51,0,0,0,0,0] 81)
for P :: J1_prog
where
Red1New:
"[| new_Addr h = Some a; P \<turnstile> C has_fields FDTs; h' = h(a\<mapsto>(Obj C (init_fields FDTs))) |]
==> P \<turnstile>1 ⟨new C, (h, l)⟩ -ε-> ⟨addr a, (h', l)⟩"
| Red1NewFail:
"new_Addr (hp s) = None
==> P \<turnstile>1 ⟨new C, s⟩ -ε-> ⟨THROW OutOfMemory, s⟩"
| New1ArrayRed:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩
==> P \<turnstile>1 ⟨newA T⌊e⌉, s⟩ -ta-> ⟨newA T⌊e'⌉, s'⟩"
| Red1NewArray:
"[| new_Addr h = Some a; i ≥ 0; h' = h(a \<mapsto> (Arr T (replicate (nat i) (default_val T)))) |]
==> P \<turnstile>1 ⟨newA T⌊Val (Intg i)⌉, (h, l)⟩ -ε-> ⟨addr a, (h', l)⟩"
| Red1NewArrayNegative:
"i < 0 ==> P \<turnstile>1 ⟨newA T⌊Val (Intg i)⌉, s⟩ -ε-> ⟨THROW NegativeArraySize, s⟩"
| Red1NewArrayFail:
"[| new_Addr h = None; i ≥ 0 |]
==> P \<turnstile>1 ⟨newA T⌊Val (Intg i)⌉, (h, l)⟩ -ε-> ⟨THROW OutOfMemory, (h, l)⟩"
| Cast1Red:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩
==> P \<turnstile>1 ⟨Cast C e, s⟩ -ta-> ⟨Cast C e', s'⟩"
| Red1Cast:
"[| typeofhp s v = ⌊U⌋; P \<turnstile> U ≤ T |]
==> P \<turnstile>1 ⟨Cast T (Val v), s⟩ -ε-> ⟨Val v, s⟩"
| Red1CastFail:
"[| typeofhp s v = ⌊U⌋; ¬ P \<turnstile> U ≤ T |]
==> P \<turnstile>1 ⟨Cast T (Val v), s⟩ -ε-> ⟨THROW ClassCast, s⟩"
| Bin1OpRed1:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨e «bop» e2, s⟩ -ta-> ⟨e' «bop» e2, s'⟩"
| Bin1OpRed2:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨(Val v) «bop» e, s⟩ -ta-> ⟨(Val v) «bop» e', s'⟩"
| Red1BinOp:
"binop bop v1 v2 = Some v ==>
P \<turnstile>1 ⟨(Val v1) «bop» (Val v2), s⟩ -ε-> ⟨Val v, s⟩"
| Red1Var:
"[| (lcl s)!V = v; V < size (lcl s) |]
==> P \<turnstile>1 ⟨Var V, s⟩ -ε-> ⟨Val v, s⟩"
| LAss1Red:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩
==> P \<turnstile>1 ⟨V:=e, s⟩ -ta-> ⟨V:=e', s'⟩"
| Red1LAss:
"V < size l
==> P \<turnstile>1 ⟨V:=(Val v), (h, l)⟩ -ε-> ⟨unit, (h, l[V := v])⟩"
| AAcc1Red1:
"P \<turnstile>1 ⟨a, s⟩ -ta-> ⟨a', s'⟩ ==> P \<turnstile>1 ⟨a⌊i⌉, s⟩ -ta-> ⟨a'⌊i⌉, s'⟩"
| AAcc1Red2:
"P \<turnstile>1 ⟨i, s⟩ -ta-> ⟨i', s'⟩ ==> P \<turnstile>1 ⟨(Val a)⌊i⌉, s⟩ -ta-> ⟨(Val a)⌊i'⌉, s'⟩"
| Red1AAccNull:
"P \<turnstile>1 ⟨null⌊Val i⌉, s⟩ -ε-> ⟨THROW NullPointer, s⟩"
| Red1AAccBounds:
"[| hp s a = Some(Arr T el); i < 0 ∨ i ≥ int (length el) |]
==> P \<turnstile>1 ⟨(addr a)⌊Val (Intg i)⌉, s⟩ -ε-> ⟨THROW ArrayIndexOutOfBounds, s⟩"
| Red1AAcc:
"[| hp s a = Some(Arr T el); i ≥ 0; i < int (length el) |]
==> P \<turnstile>1 ⟨(addr a)⌊Val (Intg i)⌉, s⟩ -ε-> ⟨Val (el ! nat i), s⟩"
| AAss1Red1:
"P \<turnstile>1 ⟨a, s⟩ -ta-> ⟨a', s'⟩ ==> P \<turnstile>1 ⟨a⌊i⌉ := e, s⟩ -ta-> ⟨a'⌊i⌉ := e, s'⟩"
| AAss1Red2:
"P \<turnstile>1 ⟨i, s⟩ -ta-> ⟨i', s'⟩ ==> P \<turnstile>1 ⟨(Val a)⌊i⌉ := e, s⟩ -ta-> ⟨(Val a)⌊i'⌉ := e, s'⟩"
| AAss1Red3:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨AAss (Val a) (Val i) e, s⟩ -ta-> ⟨(Val a)⌊Val i⌉ := e', s'⟩"
| Red1AAssNull:
"P \<turnstile>1 ⟨AAss null (Val i) (Val e), s⟩ -ε-> ⟨THROW NullPointer, s⟩"
| Red1AAssBounds:
"[| hp s a = Some(Arr T el); i < 0 ∨ i ≥ int (length el) |]
==> P \<turnstile>1 ⟨AAss (addr a) (Val (Intg i)) (Val e), s⟩ -ε-> ⟨THROW ArrayIndexOutOfBounds, s⟩"
| Red1AAssStore:
"[| hp s a = Some(Arr T el); i ≥ 0; i < int (length el); typeofhp s w = ⌊U⌋; ¬ (P \<turnstile> U ≤ T) |]
==> P \<turnstile>1 ⟨AAss (addr a) (Val (Intg i)) (Val w), s⟩ -ε-> ⟨THROW ArrayStore, s⟩"
| Red1AAss:
"[| h a = Some(Arr T el); i ≥ 0; i < int (length el); typeofh w = Some U; P \<turnstile> U ≤ T;
h' = h(a \<mapsto> (Arr T (el[nat i := w]))) |]
==> P \<turnstile>1 ⟨AAss (addr a) (Val (Intg i)) (Val w), (h, l)⟩ -ε-> ⟨unit, (h', l)⟩"
| ALength1Red:
"P \<turnstile>1 ⟨a, s⟩ -ta-> ⟨a', s'⟩ ==> P \<turnstile>1 ⟨a•length, s⟩ -ta-> ⟨a'•length, s'⟩"
| Red1ALength:
"hp s a = ⌊Arr T elem⌋ ==> P \<turnstile>1 ⟨addr a•length, s⟩ -ε-> ⟨Val (Intg (int (length elem))), s⟩"
| Red1ALengthNull:
"P \<turnstile>1 ⟨null•length, s⟩ -ε-> ⟨THROW NullPointer, s⟩"
| FAcc1Red:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨e•F{D}, s⟩ -ta-> ⟨e'•F{D}, s'⟩"
| Red1FAcc:
"[| hp s a = Some(Obj C fs); fs(F,D) = Some v |]
==> P \<turnstile>1 ⟨(addr a)•F{D}, s⟩ -ε-> ⟨Val v, s⟩"
| Red1FAccNull:
"P \<turnstile>1 ⟨null•F{D}, s⟩ -ε-> ⟨THROW NullPointer, s⟩"
| FAss1Red1:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨e•F{D}:=e2, s⟩ -ta-> ⟨e'•F{D}:=e2, s'⟩"
| FAss1Red2:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨FAss (Val v) F D e, s⟩ -ta-> ⟨Val v•F{D}:=e', s'⟩"
| Red1FAss:
"h a = Some(Obj C fs) ==>
P \<turnstile>1 ⟨FAss (addr a) F D (Val v), (h, l)⟩ -ε-> ⟨unit, (h(a \<mapsto> (Obj C (fs((F,D) \<mapsto> v)))), l)⟩"
| Red1FAssNull:
"P \<turnstile>1 ⟨FAss null F D (Val v), s⟩ -ε-> ⟨THROW NullPointer, s⟩"
| Call1Obj:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨e•M(es), s⟩ -ta-> ⟨e'•M(es), s'⟩"
| Call1Params:
"P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es',s'⟩ ==>
P \<turnstile>1 ⟨(Val v)•M(es),s⟩ -ta-> ⟨(Val v)•M(es'),s'⟩"
| Red1CallExternal:
"[| typeofhp s (Addr a) = ⌊T⌋; is_external_call P T M; P \<turnstile> ⟨a•M(vs), hp s⟩ -ta->ext ⟨va, h'⟩;
e' = extRet2J1 va; s' = (h', lcl s) |]
==> P \<turnstile>1 ⟨(addr a)•M(map Val vs), s⟩ -ta-> ⟨e', s'⟩"
| Red1CallNull:
"P \<turnstile>1 ⟨null•M(map Val vs), s⟩ -ε-> ⟨THROW NullPointer, s⟩"
| Block1Some:
"V < length x ==> P \<turnstile>1 ⟨{V:T=⌊v⌋; e}, (h, x)⟩ -ε-> ⟨{V:T=None; e}, (h, x[V := v])⟩"
| Block1Red:
"P \<turnstile>1 ⟨e, (h, x)⟩ -ta-> ⟨e', (h', x')⟩
==> P \<turnstile>1 ⟨{V:T=None; e}, (h, x)⟩ -ta-> ⟨{V:T=None; e'}, (h', x')⟩"
| Red1Block:
"P \<turnstile>1 ⟨{V:T=None; Val u}, s⟩ -ε-> ⟨Val u, s⟩"
| Synchronized1Red1:
"P \<turnstile>1 ⟨o', s⟩ -ta-> ⟨o'', s'⟩ ==> P \<turnstile>1 ⟨syncV (o') e, s⟩ -ta-> ⟨syncV (o'') e, s'⟩"
| Synchronized1Null:
"V < length xs ==> P \<turnstile>1 ⟨syncV (null) e, (h, xs)⟩ -ε-> ⟨THROW NullPointer, (h, xs[V := Null])⟩"
| Lock1Synchronized:
"[| h a = ⌊arrobj⌋; V < length xs |] ==> P \<turnstile>1 ⟨syncV (addr a) e, (h, xs)⟩ -ε\<lbrace>l Lock->a \<rbrace>\<lbrace>o Synchronization a\<rbrace>-> ⟨insyncV (a) e, (h, xs[V := Addr a])⟩"
| Synchronized1Red2:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨insyncV (a) e, s⟩ -ta-> ⟨insyncV (a) e', s'⟩"
| Unlock1Synchronized:
"[| xs ! V = Addr a'; V < length xs |] ==> P \<turnstile>1 ⟨insyncV (a) (Val v), (h, xs)⟩ -ε\<lbrace>l Unlock->a' \<rbrace>\<lbrace>o Synchronization a'\<rbrace>-> ⟨Val v, (h, xs)⟩"
| Unlock1SynchronizedNull:
"[| xs ! V = Null; V < length xs |] ==> P \<turnstile>1 ⟨insyncV (a) (Val v), (h, xs)⟩ -ε-> ⟨THROW NullPointer, (h, xs)⟩"
| Unlock1SynchronizedFail:
"[| xs ! V = Addr a'; V < length xs |]
==> P \<turnstile>1 ⟨insyncV (a) (Val v), (h, xs)⟩ -ε\<lbrace>l UnlockFail->a' \<rbrace>-> ⟨THROW IllegalMonitorState, (h, xs)⟩"
| Seq1Red:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨e;;e2, s⟩ -ta-> ⟨e';;e2, s'⟩"
| Red1Seq:
"P \<turnstile>1 ⟨Seq (Val v) e, s⟩ -ε-> ⟨e, s⟩"
| Cond1Red:
"P \<turnstile>1 ⟨b, s⟩ -ta-> ⟨b', s'⟩ ==> P \<turnstile>1 ⟨if (b) e1 else e2, s⟩ -ta-> ⟨if (b') e1 else e2, s'⟩"
| Red1CondT:
"P \<turnstile>1 ⟨if (true) e1 else e2, s⟩ -ε-> ⟨e1, s⟩"
| Red1CondF:
"P \<turnstile>1 ⟨if (false) e1 else e2, s⟩ -ε-> ⟨e2, s⟩"
| Red1While:
"P \<turnstile>1 ⟨while(b) c, s⟩ -ε-> ⟨if (b) (c;;while(b) c) else unit, s⟩"
| Throw1Red:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨throw e, s⟩ -ta-> ⟨throw e', s'⟩"
| Red1ThrowNull:
"P \<turnstile>1 ⟨throw null, s⟩ -ε-> ⟨THROW NullPointer, s⟩"
| Try1Red:
"P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> P \<turnstile>1 ⟨try e catch(C V) e2, s⟩ -ta-> ⟨try e' catch(C V) e2, s'⟩"
| Red1Try:
"P \<turnstile>1 ⟨try (Val v) catch(C V) e2, s⟩ -ε-> ⟨Val v, s⟩"
| Red1TryCatch:
"[| h a = Some(Obj D fs); P \<turnstile> D \<preceq>* C; V < length x |]
==> P \<turnstile>1 ⟨try (Throw a) catch(C V) e2, (h, x)⟩ -ε-> ⟨{V:Class C=None; e2}, (h, x[V := Addr a])⟩"
| Red1TryFail:
"[| hp s a = ⌊Obj D fs⌋; ¬ P \<turnstile> D \<preceq>* C |]
==> P \<turnstile>1 ⟨try (Throw a) catch(C V) e2, s⟩ -ε-> ⟨Throw a, s⟩"
| List1Red1:
"P \<turnstile>1 ⟨e,s⟩ -ta-> ⟨e',s'⟩ ==>
P \<turnstile>1 ⟨e#es,s⟩ [-ta->] ⟨e'#es,s'⟩"
| List1Red2:
"P \<turnstile>1 ⟨es,s⟩ [-ta->] ⟨es',s'⟩ ==>
P \<turnstile>1 ⟨Val v # es,s⟩ [-ta->] ⟨Val v # es',s'⟩"
| New1ArrayThrow: "P \<turnstile>1 ⟨newA T⌊Throw a⌉, s⟩ -ε-> ⟨Throw a, s⟩"
| Cast1Throw: "P \<turnstile>1 ⟨Cast C (Throw a), s⟩ -ε-> ⟨Throw a, s⟩"
| Bin1OpThrow1: "P \<turnstile>1 ⟨(Throw a) «bop» e2, s⟩ -ε-> ⟨Throw a, s⟩"
| Bin1OpThrow2: "P \<turnstile>1 ⟨(Val v1) «bop» (Throw a), s⟩ -ε-> ⟨Throw a, s⟩"
| LAss1Throw: "P \<turnstile>1 ⟨V:=(Throw a), s⟩ -ε-> ⟨Throw a, s⟩"
| AAcc1Throw1: "P \<turnstile>1 ⟨(Throw a)⌊i⌉, s⟩ -ε-> ⟨Throw a, s⟩"
| AAcc1Throw2: "P \<turnstile>1 ⟨(Val v)⌊Throw a⌉, s⟩ -ε-> ⟨Throw a, s⟩"
| AAss1Throw1: "P \<turnstile>1 ⟨(Throw a)⌊i⌉ := e, s⟩ -ε-> ⟨Throw a, s⟩"
| AAss1Throw2: "P \<turnstile>1 ⟨(Val v)⌊Throw a⌉ := e, s⟩ -ε-> ⟨Throw a, s⟩"
| AAss1Throw3: "P \<turnstile>1 ⟨AAss (Val v) (Val i) (Throw a), s⟩ -ε-> ⟨Throw a, s⟩"
| ALength1Throw: "P \<turnstile>1 ⟨(Throw a)•length, s⟩ -ε-> ⟨Throw a, s⟩"
| FAcc1Throw: "P \<turnstile>1 ⟨(Throw a)•F{D}, s⟩ -ε-> ⟨Throw a, s⟩"
| FAss1Throw1: "P \<turnstile>1 ⟨(Throw a)•F{D}:=e2, s⟩ -ε-> ⟨Throw a, s⟩"
| FAss1Throw2: "P \<turnstile>1 ⟨FAss (Val v) F D (Throw a), s⟩ -ε-> ⟨Throw a, s⟩"
| Call1ThrowObj: "P \<turnstile>1 ⟨(Throw a)•M(es), s⟩ -ε-> ⟨Throw a, s⟩"
| Call1ThrowParams: "[| es = map Val vs @ Throw a # es' |] ==> P \<turnstile>1 ⟨(Val v)•M(es), s⟩ -ε-> ⟨Throw a, s⟩"
| Block1Throw: "P \<turnstile>1 ⟨{V:T=None; Throw a}, s⟩ -ε-> ⟨Throw a, s⟩"
| Synchronized1Throw1: "P \<turnstile>1 ⟨syncV (Throw a) e, s⟩ -ε-> ⟨Throw a, s⟩"
| Synchronized1Throw2:
"[| xs ! V = Addr a'; V < length xs |]
==> P \<turnstile>1 ⟨insyncV (a) Throw ad, (h, xs)⟩ -ε\<lbrace>l Unlock->a' \<rbrace>\<lbrace>o Synchronization a'\<rbrace>-> ⟨Throw ad, (h, xs)⟩"
| Synchronized1Throw2Fail:
"[| xs ! V = Addr a'; V < length xs |]
==> P \<turnstile>1 ⟨insyncV (a) Throw ad, (h, xs)⟩ -ε\<lbrace>l UnlockFail->a' \<rbrace>-> ⟨THROW IllegalMonitorState, (h, xs)⟩"
| Synchronized1Throw2Null:
"[| xs ! V = Null; V < length xs |]
==> P \<turnstile>1 ⟨insyncV (a) Throw ad, (h, xs)⟩ -ε-> ⟨THROW NullPointer, (h, xs)⟩"
| Seq1Throw: "P \<turnstile>1 ⟨(Throw a);;e2, s⟩ -ε-> ⟨Throw a, s⟩"
| Cond1Throw: "P \<turnstile>1 ⟨if (Throw a) e1 else e2, s⟩ -ε-> ⟨Throw a, s⟩"
| Throw1Throw: "P \<turnstile>1 ⟨throw(Throw a), s⟩ -ε-> ⟨Throw a, s⟩"
inductive_cases red1_cases:
"P \<turnstile>1 ⟨new C, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨new T⌊e⌉, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨e «bop» e', s⟩ -ta-> ⟨e'', s'⟩"
"P \<turnstile>1 ⟨Var V, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨V:=e, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨a⌊i⌉, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨a⌊i⌉ := e, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨a•length, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨e•F{D}, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨e•F{D} := e2, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨e•M(es), s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨{V:T=vo; e}, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨syncV (o') e, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨insyncV (a) e, s⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨e;;e', s⟩ -ta-> ⟨e'', s'⟩"
"P \<turnstile>1 ⟨throw e, s ⟩ -ta-> ⟨e', s'⟩"
"P \<turnstile>1 ⟨try e catch(C V) e'', s ⟩ -ta-> ⟨e', s'⟩"
lemma red1_preserves_len: "P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> length (lcl s') = length (lcl s)"
and reds1_preserves_len: "P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> length (lcl s') = length (lcl s)"
by(induct rule: red1_reds1.inducts)(auto)
lemma reds1_preserves_elen: "P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> length es' = length es"
by(induct es arbitrary: es')(auto elim: reds1.cases)
lemma red1_no_val [dest]:
"P \<turnstile>1 ⟨Val v, s⟩ -ta-> ⟨e', s'⟩ ==> False"
by(auto elim: red1.cases)
lemma reds1_no_val [dest]:
"P \<turnstile>1 ⟨map Val vs, s⟩ [-ta->] ⟨es', s'⟩ ==> False"
apply(induct vs arbitrary: es')
apply(erule reds1.cases, auto)+
done
lemma no_reds1_map_Val_Throw [dest]:
"P \<turnstile>1 ⟨map Val vs @ Throw a # es,s⟩ [-ta->] ⟨es',s'⟩ ==> False"
by(induct vs arbitrary: es')(auto elim: reds1.cases elim!: red1_cases)
lemma red1_hext_incr: "P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> hext (hp s) (hp s')"
and reds1_hext_incr: "P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> hext (hp s) (hp s')"
apply(induct rule: red1_reds1.inducts)
apply(auto simp del: fun_upd_apply intro: hext_new hext_upd_arr hext_upd_obj dest: new_Addr_SomeD red_external_hext)
done
lemma red1_no_Throw [dest]:
"P \<turnstile>1 ⟨Throw a, s⟩ -ta-> ⟨e', s'⟩ ==> False"
by(auto elim: red1.cases)
lemma red1_max_vars_decr: "P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> max_vars e' ≤ max_vars e"
and reds1_max_varss_decr: "P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> max_varss es' ≤ max_varss es"
apply(induct rule: red1_reds1.inducts)
apply(auto)
done
lemma red1_new_thread_heap: "[|P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩; NewThread t ex h ∈ set \<lbrace>ta\<rbrace>t |] ==> h = hp s'"
and reds1_new_thread_heap: "[|P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩; NewThread t ex h ∈ set \<lbrace>ta\<rbrace>t |] ==> h = hp s'"
apply(induct rule: red1_reds1.inducts)
apply(fastsimp dest: red_ext_new_thread_heap)+
done
lemma red1_changes: "P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> e ≠ e'"
and reds1_changes: "P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> es ≠ es'"
proof(induct rule: red1_reds1.inducts)
case (Red1CallExternal s a T M vs ta va h' e' s')
thus ?case by(cases va) auto
qed auto
lemma red1_new_threadD:
"[| P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩; NewThread t x H ∈ set \<lbrace>ta\<rbrace>t |]
==> ∃a M vs va T. P \<turnstile> ⟨a•M(vs), hp s⟩ -ta->ext ⟨va, hp s'⟩ ∧ typeofhp s (Addr a) = ⌊T⌋ ∧ is_external_call P T M"
and reds1_new_threadD:
"[| P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩; NewThread t x H ∈ set \<lbrace>ta\<rbrace>t |]
==> ∃a M vs va T. P \<turnstile> ⟨a•M(vs), hp s⟩ -ta->ext ⟨va, hp s'⟩ ∧ typeofhp s (Addr a) = ⌊T⌋ ∧ is_external_call P T M"
by(induct rule: red1_reds1.inducts)(fastsimp split: heapobj.split_asm)+
primrec call1 :: "('a, 'b) exp => (addr × mname × val list) option"
and calls1 :: "('a, 'b) exp list => (addr × mname × val list) option"
where
"call1 (new C) = None"
| "call1 (newA T⌊e⌉) = call1 e"
| "call1 (Cast C e) = call1 e"
| "call1 (Val v) = None"
| "call1 (Var V) = None"
| "call1 (V:=e) = call1 e"
| "call1 (e «bop» e') = (if is_val e then call1 e' else call1 e)"
| "call1 (a⌊i⌉) = (if is_val a then call1 i else call1 a)"
| "call1 (AAss a i e) = (if is_val a then (if is_val i then call1 e else call1 i) else call1 a)"
| "call1 (a•length) = call1 a"
| "call1 (e•F{D}) = call1 e"
| "call1 (FAss e F D e') = (if is_val e then call1 e' else call1 e)"
| "call1 (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 calls1 es)
else call1 e)"
| "call1 ({V:T=vo; e}) = (case vo of None => call1 e | Some v => None)"
| "call1 (syncV (o') e) = call1 o'"
| "call1 (insyncV (a) e) = call1 e"
| "call1 (e;;e') = call1 e"
| "call1 (if (e) e1 else e2) = call1 e"
| "call1 (while(b) e) = None"
| "call1 (throw e) = call1 e"
| "call1 (try e1 catch(C V) e2) = call1 e1"
| "calls1 [] = None"
| "calls1 (e#es) = (if is_val e then calls1 es else call1 e)"
lemma call1_callE:
assumes "call1 (obj•M(pns)) = ⌊(a, M', vs)⌋"
obtains (CallObj) "call1 obj = ⌊(a, M', vs)⌋"
| (CallParams) v where "obj = Val v" "calls1 pns = ⌊(a, M', vs)⌋"
| (Call) "obj = addr a" "pns = map Val vs" "M = M'"
using assms by(auto split: split_if_asm simp add: is_vals_conv)
lemma calls1_map_Val_append [simp]:
"calls1 (map Val vs @ es) = calls1 es"
by(induct vs) simp_all
lemma calls1_map_Val [simp]:
"calls1 (map Val vs) = None"
by(induct vs) simp_all
lemma fixes e :: "('a, 'b) exp" and es :: "('a, 'b) exp list"
shows call1_imp_call: "call1 e = ⌊aMvs⌋ ==> call e = ⌊aMvs⌋"
and calls1_imp_calls: "calls1 es = ⌊aMvs⌋ ==> calls es = ⌊aMvs⌋"
by(induct e and es) auto
lemma fixes e :: "('a,'b) exp" and es :: "('a,'b) exp list"
shows inline_call_max_vars1: "call1 e = ⌊aMvs⌋ ==> max_vars (inline_call e' e) ≤ max_vars e + max_vars e'"
and inline_calls_max_varss1: "calls1 es = ⌊aMvs⌋ ==> max_varss (inline_calls e' es) ≤ max_varss es + max_vars e'"
apply(induct e and es)
apply(auto)
done
fun blocks1 :: "nat => ty list => (nat,'b) exp => (nat,'b) exp"
where
"blocks1 n [] e = e"
| "blocks1 n (T#Ts) e = {n:T=None; blocks1 (Suc n) Ts e}"
lemma expr_locks_blocks1 [simp]:
"expr_locks (blocks1 n Ts e) = expr_locks e"
by(induct n Ts e rule: blocks1.induct) simp_all
inductive Red1 :: "J1_prog => (expr1 × locals1) => (expr1 × locals1) list => heap => J1_thread_action =>
(expr1 × locals1) => (expr1 × locals1) list => heap => bool"
("_ \<turnstile>1 ((1⟨_'/_,/_⟩) -_->/ (1⟨_'/_,/_⟩))" [51,0,0,0,0,0,0,0] 81)
for P ::J1_prog
where
red1Red:
"P \<turnstile>1 ⟨e, (h, x)⟩ -ta-> ⟨e', (h', x')⟩
==> P \<turnstile>1 ⟨(e, x)/exs, h⟩ -extTA2J1 P ta-> ⟨(e', x')/exs, h'⟩"
| red1Call:
"[| call1 e = ⌊(a, M, vs)⌋; h a = ⌊Obj C fs⌋; ¬ is_external_call P (Class C) M; P \<turnstile> C sees M:Ts->T = body in D;
size vs = size Ts |]
==> P \<turnstile>1 ⟨(e, x)/exs, h⟩ -ε-> ⟨(blocks1 0 (Class D#Ts) body, Addr a # vs @ replicate (max_vars body) undefined)/(e, x)#exs, h⟩"
| red1Return:
"final e' ==> P \<turnstile>1 ⟨(e', x')/(e, x)#exs, h⟩ -ε-> ⟨(inline_call e' e, x)/exs, h⟩"
inductive IUF :: "('a, 'b) exp => ('l,'t,'m,'x,'w,'o option) thread_action => ('a, 'b) exp => bool"
and IUFs :: "('a, 'b) exp list => ('l,'t,'m,'x,'w,'o option) thread_action => ('a, 'b) exp list => bool"
where
IUFFail: "final e ==> IUF (insyncv(a) e) (ε\<lbrace>l UnlockFail->l\<rbrace>) (THROW IllegalMonitorState)"
| IUFNewArray: "IUF e ta e' ==> IUF (newA T⌊e⌉) ta (newA T⌊e'⌉)"
| IUFCast: "IUF e ta e' ==> IUF (Cast T e) ta (Cast T e')"
| IUFBinOp1: "IUF e ta e' ==> IUF (e«bop»e'') ta (e'«bop»e'')"
| IUFBinOp2: "IUF e ta e' ==> IUF (e''«bop»e) ta (e''«bop»e')"
| IUFLAss: "IUF e ta e' ==> IUF (V := e) ta (V := e')"
| IUFAAcc1: "IUF a ta a' ==> IUF (a⌊i⌉) ta (a'⌊i⌉)"
| IUFAAcc2: "IUF i ta i' ==> IUF (a⌊i⌉) ta (a⌊i'⌉)"
| IUFAAss1: "IUF a ta a' ==> IUF (a⌊i⌉ := e) ta (a'⌊i⌉ := e)"
| IUFAAss2: "IUF i ta i' ==> IUF (a⌊i⌉ := e) ta (a⌊i'⌉ := e)"
| IUFAAss3: "IUF e ta e' ==> IUF (a⌊i⌉ := e) ta (a⌊i⌉ := e')"
| IUFALength: "IUF a ta a' ==> IUF (a•length) ta (a'•length)"
| IUFFAcc: "IUF e ta e' ==> IUF (e•F{D}) ta (e'•F{D})"
| IUFFAss1: "IUF e ta e' ==> IUF (e•F{D} := e'') ta (e'•F{D} := e'')"
| IUFFAss2: "IUF e ta e' ==> IUF (e''•F{D} := e) ta (e''•F{D} := e')"
| IUFCallObj: "IUF e ta e' ==> IUF (e•M(ps)) ta (e'•M(ps))"
| IUFCallParams: "IUFs ps ta ps' ==> IUF (e•M(ps)) ta (e•M(ps'))"
| IUFBlock: "IUF e ta e' ==> IUF {V:T=vo; e} ta {V:T=vo'; e'}"
| IUFSync: "IUF e ta e' ==> IUF (syncV(e) e'') ta (syncV(e') e'')"
| IUFInSync: "IUF e ta e' ==> IUF (insyncV(a) e) ta (insyncV(a) e')"
| IUFSeq: "IUF e ta e' ==> IUF (e;;e'') ta (e';;e'')"
| IUFCond: "IUF b ta b' ==> IUF (if (b) e else e') ta (if (b') e else e')"
| IUFThrow: "IUF e ta e' ==> IUF (throw e) ta (throw e')"
| IUFTry: "IUF e ta e' ==> IUF (try e catch(C V) e'') ta (try e' catch(C V) e'')"
| IUFList1: "IUF e ta e' ==> IUFs (e # es) ta (e' # es)"
| IUFList2: "IUFs es ta es' ==> IUFs (e # es) ta (e # es')"
inductive_cases IUF_cases [elim!]:
"IUF (newA T⌊e⌉) ta e'"
"IUF e ta (newA T⌊e'⌉)"
"IUF (Cast T e) ta e'"
"IUF e ta (Cast T e')"
"IUF (e«bop»e') ta e''"
"IUF e ta (e'«bop»e'')"
"IUF (V := e) ta e'"
"IUF e' ta (V := e')"
"IUF (a⌊i⌉) ta e"
"IUF e ta (a⌊i⌉)"
"IUF (AAss a i e) ta e'"
"IUF e ta (AAss a i e')"
"IUF (a•length) ta e"
"IUF e ta (a•length)"
"IUF (e•F{D}) ta e'"
"IUF e ta (e'•F{D})"
"IUF (FAss e F D e') ta e''"
"IUF e ta (FAss e' F D e'')"
"IUF (e•M(ps)) ta e'"
"IUF e ta (e'•M(ps))"
"IUF {V:T=vo; e} ta e'"
"IUF e ta {v:T=vo; e'}"
"IUF (syncV(e) e') ta e''"
"IUF e ta (syncV(e') e'')"
"IUF (insyncV(a) e) ta e'"
"IUF e ta (insyncV(a) e')"
"IUF (e;;e') ta e''"
"IUF e ta (e';;e'')"
"IUF (if (b) e else e') ta e''"
"IUF e ta (if (b) e' else e'')"
"IUF (throw e) ta e'"
"IUF e ta (throw e')"
"IUF (try e catch(C V) e') ta e''"
"IUF e ta (try e' catch(C v) e'')"
inductive_cases IUFs_cases [elim!]:
"IUFs (e # es) ta es'"
"IUFs es ta (e # es')"
lemma IUF_const_exprs [iff]:
"IUF (new C) ta e = False"
"IUF e ta (new C) = False"
"IUF (Var V) ta e = False"
"IUF e ta (Var V) = False"
"IUF (Val v) ta e = False"
"IUF e ta (Val v) = False"
"IUF (while(b) c) ta e = False"
"IUF e ta (while(b) c) = False"
"IUFs [] ta es = False"
"IUFs es ta [] = False"
apply(auto elim: IUF.cases IUFs.cases)
done
lemma IUFs_map_Val [iff]:
"IUFs (map Val vs) ta es = False"
"IUFs es ta (map Val vs) = False"
by(induct vs arbitrary: es) auto
declare IUF_IUFs.intros [intro!]
lemma IUF_simps [simp]:
"IUF (newA T⌊e⌉) ta (newA T⌊e'⌉) <-> IUF e ta e'"
"IUF (Cast T e) ta (Cast T e') <-> IUF e ta e'"
"IUF (e«bop»e') ta (e''«bop»e''') <-> IUF e ta e'' ∧ e' = e''' ∨ IUF e' ta e''' ∧ e = e''"
"IUF (V := e) ta (V := e') <-> IUF e ta e'"
"IUF (a⌊i⌉) ta (a'⌊i'⌉) <-> IUF a ta a' ∧ i = i' ∨ IUF i ta i' ∧ a = a'"
"IUF (AAss a i e) ta (AAss a' i' e') <-> IUF a ta a' ∧ i = i' ∧ e = e' ∨ IUF i ta i' ∧ a = a' ∧ e = e' ∨ IUF e ta e' ∧ a = a' ∧ i = i'"
"IUF (a•length) ta (a'•length) <-> IUF a ta a'"
"IUF (e•F{D}) ta (e'•F{D}) <-> IUF e ta e'"
"IUF (FAss e F D e') ta (FAss e'' F D e''') <-> IUF e ta e'' ∧ e' = e''' ∨ IUF e' ta e''' ∧ e = e''"
"IUF (e•M(ps)) ta (e'•M(ps')) <-> IUF e ta e' ∧ ps = ps' ∨ IUFs ps ta ps' ∧ e = e'"
"IUF {V:T=vo; e} ta {V:T=vo'; e'} <-> IUF e ta e'"
"IUF (syncV(e) e') ta (syncV(e'') e''') <-> IUF e ta e'' ∧ e' = e'''"
"IUF (insyncV(ad) e) ta (insyncV(ad) e') <-> IUF e ta e'"
"IUF (e;;e') ta (e'';;e''') <-> IUF e ta e'' ∧ e' = e'''"
"IUF (if (b) e else e') ta (if (b') e'' else e''') <-> IUF b ta b' ∧ e = e'' ∧ e' = e'''"
"IUF (throw e) ta (throw e') <-> IUF e ta e'"
"IUF (try e catch(C V) e') ta (try e'' catch(C V) e''') <-> IUF e ta e'' ∧ e' = e'''"
by auto
lemma IUF_same_False [iff]:
fixes e :: "('a, 'b) exp" and es :: "('a, 'b) exp list"
shows "IUF e ta e = False" and "IUFs es ta es = False"
proof -
have "IUF e ta e ==> False" and "IUFs es ta es ==> False"
by(induct e and es) auto
thus "IUF e ta e = False" "IUFs es ta es = False" by auto
qed
lemma IUF_taD:
fixes e :: "('a, 'b) exp" and es :: "('a, 'b) exp list"
shows "IUF e ta e' ==> ∃l. ta = ε\<lbrace>l UnlockFail->l\<rbrace>"
and "IUFs es ta es' ==> ∃l. ta = ε\<lbrace>l UnlockFail->l\<rbrace>"
by(induct rule: IUF_IUFs.inducts) auto
definition IUFL :: "(('a, 'b) exp × 'c) => 'd => ('l,'t,'x,'m,'w,'o option) thread_action => (('a, 'b) exp × 'c) => 'd => bool"
where "IUFL ex exs ta ex' exs' <-> exs = exs' ∧ IUF (fst ex) ta (fst ex')"
abbreviation mred1' :: "J1_prog => (addr,addr,(expr1 × locals1) × (expr1 × locals1) list,heap,addr,obs_event) semantics"
where "mred1' P ≡ λ((ex, exs), h) ta ((ex', exs'), h'). P \<turnstile>1 ⟨ex/exs, h⟩ -ta-> ⟨ex'/exs', h'⟩ ∧ ¬ IUFL ex exs ta ex' exs'"
abbreviation mred1 :: "J1_prog => (addr,addr,(expr1 × locals1) × (expr1 × locals1) list,heap,addr,obs_event) semantics"
where "mred1 P ≡ λ((ex, exs), h) ta ((ex', exs'), h'). P \<turnstile>1 ⟨ex/exs, h⟩ -ta-> ⟨ex'/exs', h'⟩"
lemma red1_call_synthesized: "[| P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩; call1 e = ⌊aMvs⌋ |] ==> synthesized_call P (hp s) aMvs" -- "Move to J1"
and reds1_calls_synthesized: "[| P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩; calls1 es = ⌊aMvs⌋ |] ==> synthesized_call P (hp s) aMvs"
apply(induct rule: red1_reds1.inducts)
apply(auto split: split_if_asm simp add: is_vals_conv append_eq_map_conv synthesized_call_conv)
done
section {* Silent moves *}
primrec τmove1 :: "'m prog => heap => ('a, 'b) exp => bool"
and τmoves1 :: "'m prog => heap => ('a, 'b) exp list => bool"
where
"τmove1 P h (new C) <-> False"
| "τmove1 P h (newA T⌊e⌉) <-> τmove1 P h e ∨ (∃a. e = Throw a)"
| "τmove1 P h (Cast U e) <-> τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove1 P h (e «bop» e') <-> τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧ (τmove1 P h e' ∨ (∃a. e' = Throw a) ∨ (∃v. e' = Val v)))"
| "τmove1 P h (Val v) <-> False"
| "τmove1 P h (Var V) <-> True"
| "τmove1 P h (V := e) <-> τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove1 P h (a⌊i⌉) <-> τmove1 P h a ∨ (∃ad. a = Throw ad) ∨ (∃v. a = Val v ∧ (τmove1 P h i ∨ (∃a. i = Throw a)))"
| "τmove1 P h (AAss a i e) <-> τmove1 P h a ∨ (∃ad. a = Throw ad) ∨ (∃v. a = Val v ∧ (τmove1 P h i ∨ (∃a. i = Throw a) ∨ (∃v. i = Val v ∧ (τmove1 P h e ∨ (∃a. e = Throw a)))))"
| "τmove1 P h (a•length) <-> τmove1 P h a ∨ (∃ad. a = Throw ad)"
| "τmove1 P h (e•F{D}) <-> τmove1 P h e ∨ (∃a. e = Throw a)"
| "τmove1 P h (FAss e F D e') <-> τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧ (τmove1 P h e' ∨ (∃a. e' = Throw a)))"
| "τmove1 P h (e•M(es)) <-> τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧
(τmoves1 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)))))"
| "τmove1 P h ({V:T=vo; e}) <-> (τmove1 P h e ∧ vo = None) ∨ (((∃a. e = Throw a) ∨ (∃v. e = Val v)) ∧ vo = None) ∨ vo ≠ None"
| "τmove1 P h (syncV'(e) e') <-> τmove1 P h e ∨ (∃a. e = Throw a)"
| "τmove1 P h (insyncV'(ad) e) <-> τmove1 P h e"
| "τmove1 P h (e;;e') <-> τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove1 P h (if (e) e' else e'') <-> τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove1 P h (while (e) e') = True"
| "τmove1 P h (throw e) <-> τmove1 P h e ∨ (∃a. e = Throw a) ∨ e = null"
| "τmove1 P h (try e catch(C V) e') <-> τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmoves1 P h [] <-> False"
| "τmoves1 P h (e # es) <-> τmove1 P h e ∨ (∃v. e = Val v ∧ τmoves1 P h es)"
lemma τmove1_τmoves1_intros:
fixes e :: "('a, 'b) exp" and es :: "('a, 'b) exp list"
shows τmove1NewArray: "τmove1 P h e ==> τmove1 P h (newA T⌊e⌉)"
and τmove1Cast: "τmove1 P h e ==> τmove1 P h (Cast U e)"
and τmove1CastRed: "τmove1 P h (Cast U (Val v))"
and τmove1BinOp1: "τmove1 P h e ==> τmove1 P h (e«bop»e')"
and τmove1BinOp2: "τmove1 P h e ==> τmove1 P h (Val v«bop»e)"
and τmove1BinOp: "τmove1 P h (Val v«bop»Val v')"
and τmove1Var: "τmove1 P h (Var V)"
and τmove1LAss: "τmove1 P h e ==> τmove1 P h (V := e)"
and τmove1LAssRed: "τmove1 P h (V := Val v)"
and τmove1AAcc1: "τmove1 P h e ==> τmove1 P h (e⌊e'⌉)"
and τmove1AAcc2: "τmove1 P h e ==> τmove1 P h (Val v⌊e⌉)"
and τmove1AAss1: "τmove1 P h e ==> τmove1 P h (AAss e e' e'')"
and τmove1AAss2: "τmove1 P h e ==> τmove1 P h (AAss (Val v) e e')"
and τmove1AAss3: "τmove1 P h e ==> τmove1 P h (AAss (Val v) (Val v') e)"
and τmove1ALength: "τmove1 P h e ==> τmove1 P h (e•length)"
and τmove1FAcc: "τmove1 P h e ==> τmove1 P h (e•F{D})"
and τmove1FAss1: "τmove1 P h e ==> τmove1 P h (FAss e F D e')"
and τmove1FAss2: "τmove1 P h e ==> τmove1 P h (FAss (Val v) F D e)"
and τmove1CallObj: "τmove1 P h obj ==> τmove1 P h (obj•M(ps))"
and τmove1CallParams: "τmoves1 P h ps ==> τmove1 P h (Val v•M(ps))"
and τmove1Call: "(!!T. typeofh v = ⌊T⌋ ==> ¬ is_external_call P T M) ==> τmove1 P h (Val v•M(map Val vs))"
and τmove1BlockSome: "τmove1 P h {V:T=⌊v⌋; e}"
and τmove1Block: "τmove1 P h e ==> τmove1 P h {V:T=None; e}"
and τmove1BlockRed: "τmove1 P h {V:T=None; Val v}"
and τmove1Sync: "τmove1 P h e ==> τmove1 P h (syncV' (e) e')"
and τmove1InSync: "τmove1 P h e ==> τmove1 P h (insyncV' (a) e)"
and τmove1Seq: "τmove1 P h e ==> τmove1 P h (e;;e')"
and τmove1SeqRed: "τmove1 P h (Val v;; e)"
and τmove1Cond: "τmove1 P h e ==> τmove1 P h (if (e) e1 else e2)"
and τmove1CondRed: "τmove1 P h (if (Val v) e1 else e2)"
and τmove1WhileRed: "τmove1 P h (while (c) e)"
and τmove1Throw: "τmove1 P h e ==> τmove1 P h (throw e)"
and τmove1ThrowNull: "τmove1 P h (throw null)"
and τmove1Try: "τmove1 P h e ==> τmove1 P h (try e catch(C V) e'')"
and τmove1TryRed: "τmove1 P h (try Val v catch(C V) e)"
and τmove1TryThrow: "τmove1 P h (try Throw a catch(C V) e)"
and τmove1NewArrayThrow: "τmove1 P h (newA T⌊Throw a⌉)"
and τmove1CastThrow: "τmove1 P h (Cast T (Throw a))"
and τmove1BinOpThrow1: "τmove1 P h (Throw a «bop» e2)"
and τmove1BinOpThrow2: "τmove1 P h (Val v «bop» Throw a)"
and τmove1LAssThrow: "τmove1 P h (V:=(Throw a))"
and τmove1AAccThrow1: "τmove1 P h (Throw a⌊e⌉)"
and τmove1AAccThrow2: "τmove1 P h (Val v⌊Throw a⌉)"
and τmove1AAssThrow1: "τmove1 P h (AAss (Throw a) e e')"
and τmove1AAssThrow2: "τmove1 P h (AAss (Val v) (Throw a) e')"
and τmove1AAssThrow3: "τmove1 P h (AAss (Val v) (Val v') (Throw a))"
and τmove1ALengthThrow: "τmove1 P h (Throw a•length)"
and τmove1FAccThrow: "τmove1 P h (Throw a•F{D})"
and τmove1FAssThrow1: "τmove1 P h (Throw a•F{D} := e)"
and τmove1FAssThrow2: "τmove1 P h (FAss (Val v) F D (Throw a))"
and τmove1CallThrowObj: "τmove1 P h (Throw a•M(es))"
and τmove1CallThrowParams: "τmove1 P h (Val v•M(map Val vs @ Throw a # es))"
and τmove1BlockThrow: "τmove1 P h {V:T=None; Throw a}"
and τmove1SyncThrow: "τmove1 P h (syncV' (Throw a) e)"
and τmove1SeqThrow: "τmove1 P h (Throw a;;e)"
and τmove1CondThrow: "τmove1 P h (if (Throw a) e1 else e2)"
and τmove1ThrowThrow: "τmove1 P h (throw (Throw a))"
and τmoves1Hd: "τmove1 P h e ==> τmoves1 P h (e # es)"
and τmoves1Tl: "τmoves1 P h es ==> τmoves1 P h (Val v # es)"
by fastsimp+
lemma τmoves1_map_Val [dest!]:
"τmoves1 P h (map Val es) ==> False"
by(induct es)(auto)
lemma fixes e :: "('a, 'b) exp" and es :: "('a, 'b) exp list"
shows τmove1_not_call1: "call1 e = ⌊aMvs⌋ ==> τmove1 P h e <-> ¬ synthesized_call P h aMvs"
and τmoves1_not_calls1: "calls1 es = ⌊aMvs⌋ ==> τmoves1 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 red1_τ_taD: "[| P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩; τmove1 P (hp s) e |] ==> ta = ε"
and reds1_τ_taD: "[| P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩; τmoves1 P (hp s) es |] ==> ta = ε"
apply(induct rule: red1_reds1.inducts)
apply(fastsimp simp add: map_eq_append_conv)+
done
lemma τmove1_heap_unchanged: "[| P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩; τmove1 P (hp s) e |] ==> hp s' = hp s"
and τmoves1_heap_unchanged: "[| P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩; τmoves1 P (hp s) es |] ==> hp s' = hp s"
apply(induct rule: red1_reds1.inducts)
apply(auto)
apply(fastsimp simp add: map_eq_append_conv)
done
lemma red1_hext:
"[| P \<turnstile>1 ⟨e, s⟩ -ε-> ⟨e', s'⟩; hp s = hp s'; hext (hp s) h; τmove1 P (hp s) e |]
==> P \<turnstile>1 ⟨e, (h, lcl s)⟩ -ε-> ⟨e', (h, lcl s')⟩"
and reds1_hext:
"[| P \<turnstile>1 ⟨es, s⟩ [-ε->] ⟨es', s'⟩; hp s = hp s'; hext (hp s) h; τmoves1 P (hp s) es |]
==> P \<turnstile>1 ⟨es, (h, lcl s)⟩ [-ε->] ⟨es', (h, lcl s')⟩"
proof(induct e s ta≡"ε :: external_thread_action" e' s'
and es s ta≡"ε :: external_thread_action" es' s'
rule: red1_reds1.inducts)
case Red1New thus ?case by(fastsimp dest: new_Addr_SomeD simp add: expand_fun_eq split: split_if_asm)
next
case Red1NewFail thus ?case
by(fastsimp simp add: new_Addr_def dest: hext_objarrD split: split_if_asm intro!: red1_reds1.Red1NewFail)
next
case Red1Cast thus ?case by(fastsimp dest: hext_typeof_mono intro: red1_reds1.Red1Cast)
next
case Red1CastFail thus ?case by(fastsimp dest: hext_typeof_mono intro: red1_reds1.Red1CastFail)
next
case Red1TryCatch thus ?case by(auto dest: hext_objD intro: red1_reds1.intros)
next
case Red1TryFail thus ?case by(auto dest!: hext_objD)(auto intro: red1_reds1.intros)
next
case Red1CallExternal thus ?case by(fastsimp simp add: map_eq_append_conv)
qed(fastsimp intro: red1_reds1.intros simp add: expand_finfun_eq expand_fun_eq finfun_upd_apply split: split_if_asm)+
fun τMove1 :: "'m prog => heap => (('a, 'b) exp × 'c) × (('a, 'b) exp × 'd) list => bool"
where
"τMove1 P h ((e, x), exs) = (τmove1 P h e ∨ final e)"
lemma τMove1_iff:
"τMove1 P h exexs <-> (let ((e, _), _) = exexs in τmove1 P h e ∨ final e)"
by(cases exexs)(auto)
definition τred1 :: "J1_prog => heap => (expr1 × locals1) => (expr1 × locals1) => bool"
where "τred1 P h exs e'xs' = (P \<turnstile>1 ⟨fst exs, (h, snd exs)⟩ -ε-> ⟨fst e'xs', (h, snd e'xs')⟩ ∧ τmove1 P h (fst exs))"
definition τreds1 :: "J1_prog => heap => (expr1 list × locals1) => (expr1 list × locals1) => bool"
where "τreds1 P h esxs es'xs' = (P \<turnstile>1 ⟨fst esxs, (h, snd esxs)⟩ [-ε->] ⟨fst es'xs', (h, snd es'xs')⟩ ∧ τmoves1 P h (fst esxs))"
abbreviation τred1t :: "J1_prog => heap => (expr1 × locals1) => (expr1 × locals1) => bool"
where "τred1t P h ≡ (τred1 P h)^++"
abbreviation τreds1t :: "J1_prog => heap => (expr1 list × locals1) => (expr1 list × locals1) => bool"
where "τreds1t P h ≡ (τreds1 P h)^++"
abbreviation τred1r :: "J1_prog => heap => (expr1 × locals1) => (expr1 × locals1) => bool"
where "τred1r P h ≡ (τred1 P h)^**"
abbreviation τreds1r :: "J1_prog => heap => (expr1 list × locals1) => (expr1 list × locals1) => bool"
where "τreds1r P h ≡ (τreds1 P h)^**"
lemma τred1_iff [iff]:
"τred1 P h (e, xs) (e', xs') = (P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩ ∧ τmove1 P h e)"
by(simp add: τred1_def)
lemma τreds1_iff [iff]:
"τreds1 P h (es, xs) (es', xs') = (P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩ ∧ τmoves1 P h es)"
by(simp add: τreds1_def)
lemma τred1t_1step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e |]
==> τred1t P h (e, xs) (e', xs')"
by(blast intro: tranclp.r_into_trancl)
lemma τred1t_2step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e;
P \<turnstile>1 ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove1 P h e' |]
==> τred1t P h (e, xs) (e'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τred1t_1step])
lemma τred1t_3step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e;
P \<turnstile>1 ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove1 P h e';
P \<turnstile>1 ⟨e'', (h, xs'')⟩ -ε-> ⟨e''', (h, xs''')⟩; τmove1 P h e'' |]
==> τred1t P h (e, xs) (e''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τred1t_2step])
lemma τreds1t_1step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es |]
==> τreds1t P h (es, xs) (es', xs')"
by(blast intro: tranclp.r_into_trancl)
lemma τreds1t_2step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es;
P \<turnstile>1 ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves1 P h es' |]
==> τreds1t P h (es, xs) (es'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds1t_1step])
lemma τreds1t_3step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es;
P \<turnstile>1 ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves1 P h es';
P \<turnstile>1 ⟨es'', (h, xs'')⟩ [-ε->] ⟨es''', (h, xs''')⟩; τmoves1 P h es'' |]
==> τreds1t P h (es, xs) (es''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds1t_2step])
lemma τred1r_1step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e |]
==> τred1r P h (e, xs) (e', xs')"
by(blast intro: r_into_rtranclp)
lemma τred1r_2step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e;
P \<turnstile>1 ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove1 P h e' |]
==> τred1r P h (e, xs) (e'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred1r_1step])
lemma τred1r_3step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e;
P \<turnstile>1 ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove1 P h e';
P \<turnstile>1 ⟨e'', (h, xs'')⟩ -ε-> ⟨e''', (h, xs''')⟩; τmove1 P h e'' |]
==> τred1r P h (e, xs) (e''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred1r_2step])
lemma τreds1r_1step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es |]
==> τreds1r P h (es, xs) (es', xs')"
by(blast intro: r_into_rtranclp)
lemma τreds1r_2step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es;
P \<turnstile>1 ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves1 P h es' |]
==> τreds1r P h (es, xs) (es'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds1r_1step])
lemma τreds1r_3step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es;
P \<turnstile>1 ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves1 P h es';
P \<turnstile>1 ⟨es'', (h, xs'')⟩ [-ε->] ⟨es''', (h, xs''')⟩; τmoves1 P h es'' |]
==> τreds1r P h (es, xs) (es''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds1r_2step])
lemma τred1t_preserves_len: "τred1t P h (e, xs) (e', xs') ==> length xs' = length xs"
by(induct rule: tranclp_induct2)(auto dest: red1_preserves_len)
lemma τred1r_preserves_len: "τred1r P h (e, xs) (e', xs') ==> length xs' = length xs"
by(induct rule: rtranclp_induct2)(auto dest: red1_preserves_len)
lemma τred1t_inj_τreds1t: "τred1t P h (e, xs) (e', xs') ==> τreds1t P h (e # es, xs) (e' # es, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl List1Red1 τmoves1Hd)
lemma τreds1t_cons_τreds1t: "τreds1t P h (es, xs) (es', xs') ==> τreds1t P h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl List1Red2 τmoves1Tl)
lemma τred1r_inj_τreds1r: "τred1r P h (e, xs) (e', xs') ==> τreds1r P h (e # es, xs) (e' # es, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl List1Red1 τmoves1Hd)
lemma τreds1r_cons_τreds1r: "τreds1r P h (es, xs) (es', xs') ==> τreds1r P h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl List1Red2 τmoves1Tl)
lemma NewArray_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl New1ArrayRed τmove1NewArray)
lemma Cast_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Cast1Red τmove1Cast)
lemma BinOp_τred1t_xt1:
"τred1t P h (e1, xs) (e1', xs') ==> τred1t P h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Bin1OpRed1 τmove1BinOp1)
lemma BinOp_τred1t_xt2:
"τred1t P h (e2, xs) (e2', xs') ==> τred1t P h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Bin1OpRed2 τmove1BinOp2)
lemma LAss_τred1t:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (V := e, xs) (V := e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl LAss1Red τmove1LAss)
lemma AAcc_τred1t_xt1:
"τred1t P h (a, xs) (a', xs') ==> τred1t P h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAcc1Red1 τmove1AAcc1)
lemma AAcc_τred1t_xt2:
"τred1t P h (i, xs) (i', xs') ==> τred1t P h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAcc1Red2 τmove1AAcc2)
lemma AAss_τred1t_xt1:
"τred1t P h (a, xs) (a', xs') ==> τred1t P h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAss1Red1 τmove1AAss1)
lemma AAss_τred1t_xt2:
"τred1t P h (i, xs) (i', xs') ==> τred1t P h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAss1Red2 τmove1AAss2)
lemma AAss_τred1t_xt3:
"τred1t P h (e, xs) (e', xs') ==> τred1t 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 AAss1Red3 τmove1AAss3)
lemma ALength_τred1t_xt:
"τred1t P h (a, xs) (a', xs') ==> τred1t P h (a•length, xs) (a'•length, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ALength1Red τmove1ALength)
lemma FAcc_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (e•F{D}, xs) (e'•F{D}, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAcc1Red τmove1FAcc)
lemma FAss_τred1t_xt1:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (e•F{D} := e2, xs) (e'•F{D} := e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAss1Red1 τmove1FAss1)
lemma FAss_τred1t_xt2:
"τred1t P h (e, xs) (e', xs') ==> τred1t 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 FAss1Red2 τmove1FAss2)
lemma Call_τred1t_obj:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (e•M(ps), xs) (e'•M(ps), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Call1Obj τmove1CallObj)
lemma Call_τred1t_param:
"τreds1t P h (es, xs) (es', xs') ==> τred1t P h (Val v•M(es), xs) (Val v•M(es'), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Call1Params τmove1CallParams)
lemma Block_None_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h ({V:T=None; e}, xs) ({V:T=None; e'}, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl τmove1Block elim!: Block1Red)
lemma Block_τred1t_Some:
"[| τred1t P h (e, xs[V := v]) (e', xs'); V < length xs |]
==> τred1t P h ({V:Ty=⌊v⌋; e}, xs) ({V:Ty=None; e'}, xs')"
by(blast intro: tranclp_into_tranclp2 Block1Some τmove1BlockSome Block_None_τred1t_xt)
lemma Sync_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (syncV (e) e2, xs) (syncV (e') e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Synchronized1Red1 τmove1Sync)
lemma InSync_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (insyncV (a) e, xs) (insyncV (a) e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Synchronized1Red2 τmove1InSync)
lemma Seq_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Seq1Red τmove1Seq)
lemma Cond_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t 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 Cond1Red τmove1Cond)
lemma Throw_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t P h (throw e, xs) (throw e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Throw1Red τmove1Throw)
lemma Try_τred1t_xt:
"τred1t P h (e, xs) (e', xs') ==> τred1t 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 Try1Red τmove1Try)
lemma NewArray_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl New1ArrayRed τmove1NewArray)
lemma Cast_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Cast1Red τmove1Cast)
lemma BinOp_τred1r_xt1:
"τred1r P h (e1, xs) (e1', xs') ==> τred1r P h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Bin1OpRed1 τmove1BinOp1)
lemma BinOp_τred1r_xt2:
"τred1r P h (e2, xs) (e2', xs') ==> τred1r P h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Bin1OpRed2 τmove1BinOp2)
lemma LAss_τred1r:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (V := e, xs) (V := e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl LAss1Red τmove1LAss)
lemma AAcc_τred1r_xt1:
"τred1r P h (a, xs) (a', xs') ==> τred1r P h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAcc1Red1 τmove1AAcc1)
lemma AAcc_τred1r_xt2:
"τred1r P h (i, xs) (i', xs') ==> τred1r P h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAcc1Red2 τmove1AAcc2)
lemma AAss_τred1r_xt1:
"τred1r P h (a, xs) (a', xs') ==> τred1r P h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAss1Red1 τmove1AAss1)
lemma AAss_τred1r_xt2:
"τred1r P h (i, xs) (i', xs') ==> τred1r P h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAss1Red2 τmove1AAss2)
lemma AAss_τred1r_xt3:
"τred1r P h (e, xs) (e', xs') ==> τred1r 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 AAss1Red3 τmove1AAss3)
lemma ALength_τred1r_xt:
"τred1r P h (a, xs) (a', xs') ==> τred1r P h (a•length, xs) (a'•length, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ALength1Red τmove1ALength)
lemma FAcc_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (e•F{D}, xs) (e'•F{D}, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAcc1Red τmove1FAcc)
lemma FAss_τred1r_xt1:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (e•F{D} := e2, xs) (e'•F{D} := e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAss1Red1 τmove1FAss1)
lemma FAss_τred1r_xt2:
"τred1r P h (e, xs) (e', xs') ==> τred1r 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 FAss1Red2 τmove1FAss2)
lemma Call_τred1r_obj:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (e•M(ps), xs) (e'•M(ps), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Call1Obj τmove1CallObj)
lemma Call_τred1r_param:
"τreds1r P h (es, xs) (es', xs') ==> τred1r P h (Val v•M(es), xs) (Val v•M(es'), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Call1Params τmove1CallParams)
lemma Block_None_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h ({V:T=None; e}, xs) ({V:T=None; e'}, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl τmove1Block elim!: Block1Red)
lemma Block_τred1r_Some:
"[| τred1r P h (e, xs[V := v]) (e', xs'); V < length xs |]
==> τred1r P h ({V:Ty=⌊v⌋; e}, xs) ({V:Ty=None; e'}, xs')"
by(blast intro: converse_rtranclp_into_rtranclp Block1Some τmove1BlockSome Block_None_τred1r_xt)
lemma Sync_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (syncV (e) e2, xs) (syncV (e') e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Synchronized1Red1 τmove1Sync)
lemma InSync_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (insyncV (a) e, xs) (insyncV (a) e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Synchronized1Red2 τmove1InSync)
lemma Seq_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Seq1Red τmove1Seq)
lemma Cond_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r 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 Cond1Red τmove1Cond)
lemma Throw_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r P h (throw e, xs) (throw e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Throw1Red τmove1Throw)
lemma Try_τred1r_xt:
"τred1r P h (e, xs) (e', xs') ==> τred1r 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 Try1Red τmove1Try)
lemma τred1t_ThrowD [dest]: "τred1t P h (Throw a, xs) (e'', xs'') ==> e'' = Throw a ∧ xs'' = xs"
by(induct rule: tranclp_induct2)(auto)
lemma τred1r_ThrowD [dest]: "τred1r P h (Throw a, xs) (e'', xs'') ==> e'' = Throw a ∧ xs'' = xs"
by(induct rule: rtranclp_induct2)(auto)
definition τRed1 :: "J1_prog => heap => (expr1 × locals1) × ((expr1 × locals1) list) =>
(expr1 × locals1) × ((expr1 × locals1) list) => bool"
where "τRed1 P h exexs ex'exs' = (P \<turnstile>1 ⟨fst exexs/snd exexs, h⟩ -ε-> ⟨fst ex'exs'/snd ex'exs', h⟩ ∧ τMove1 P h exexs)"
lemma τRed1_conv [iff]:
"τRed1 P h (ex, exs) (ex', exs') = (P \<turnstile>1 ⟨ex/exs, h⟩ -ε-> ⟨ex'/exs', h⟩ ∧ τMove1 P h (ex, exs))"
by(simp add: τRed1_def)
abbreviation τRed1t :: "J1_prog => heap => (expr1 × locals1) × ((expr1 × locals1) list) =>
(expr1 × locals1) × ((expr1 × locals1) list) => bool"
where "τRed1t P h ≡ (τRed1 P h)^++"
abbreviation τRed1r :: "J1_prog => heap => (expr1 × locals1) × ((expr1 × locals1) list) =>
(expr1 × locals1) × ((expr1 × locals1) list) => bool"
where "τRed1r P h ≡ (τRed1 P h)^**"
lemma τred1t_into_τRed1t:
"τred1t P h (e, xs) (e'', xs'') ==> τRed1t P h ((e, xs), exs) ((e'', xs''), exs)"
by(induct rule: tranclp_induct2)(fastsimp dest: red1Red intro: τmove1Block tranclp.intros)+
lemma τred1r_into_τRed1r:
"τred1r P h (e, xs) (e'', xs'') ==> τRed1r P h ((e, xs), exs) ((e'', xs''), exs)"
by(induct rule: rtranclp_induct2)(fastsimp dest: red1Red intro: τmove1Block rtranclp.intros)+
lemma red1_max_vars: "P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> max_vars e' ≤ max_vars e"
and reds1_max_varss: "P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> max_varss es' ≤ max_varss es"
by(induct rule: red1_reds1.inducts) auto
lemma τred1t_max_vars: "τred1t P h (e, xs) (e', xs') ==> max_vars e' ≤ max_vars e"
by(induct rule: tranclp_induct2)(auto dest: red1_max_vars)
lemma τred1r_max_vars: "τred1r P h (e, xs) (e', xs') ==> max_vars e' ≤ max_vars e"
by(induct rule: rtranclp_induct2)(auto dest: red1_max_vars)
definition τred1' :: "J1_prog => heap => (expr1 × locals1) => (expr1 × locals1) => bool"
where
"τred1' P h exs e'xs' =
(P \<turnstile>1 ⟨fst exs, (h, snd exs)⟩ -ε-> ⟨fst e'xs', (h, snd e'xs')⟩ ∧ τmove1 P h (fst exs) ∧ ¬ IUF (fst exs) (ε :: J1_thread_action) (fst e'xs'))"
definition τreds1' :: "J1_prog => heap => (expr1 list × locals1) => (expr1 list × locals1) => bool"
where
"τreds1' P h esxs es'xs' =
(P \<turnstile>1 ⟨fst esxs, (h, snd esxs)⟩ [-ε->] ⟨fst es'xs', (h, snd es'xs')⟩ ∧ τmoves1 P h (fst esxs) ∧ ¬ IUFs (fst esxs) (ε:: J1_thread_action) (fst es'xs'))"
abbreviation τred1't :: "J1_prog => heap => (expr1 × locals1) => (expr1 × locals1) => bool"
where "τred1't P h ≡ (τred1' P h)^++"
abbreviation τreds1't :: "J1_prog => heap => (expr1 list × locals1) => (expr1 list × locals1) => bool"
where "τreds1't P h ≡ (τreds1' P h)^++"
abbreviation τred1'r :: "J1_prog => heap => (expr1 × locals1) => (expr1 × locals1) => bool"
where "τred1'r P h ≡ (τred1' P h)^**"
abbreviation τreds1'r :: "J1_prog => heap => (expr1 list × locals1) => (expr1 list × locals1) => bool"
where "τreds1'r P h ≡ (τreds1' P h)^**"
lemma τred1'_iff [iff]:
"τred1' P h (e, xs) (e', xs') = (P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩ ∧ τmove1 P h e ∧ ¬ IUF e (ε :: J1_thread_action) e')"
by(simp add: τred1'_def)
lemma τreds1'_iff [iff]:
"τreds1' P h (es, xs) (es', xs') = (P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩ ∧ τmoves1 P h es ∧ ¬ IUFs es (ε :: J1_thread_action) es')"
by(simp add: τreds1'_def)
lemma τred1't_1step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e; ¬ IUF e (ε :: J1_thread_action) e' |]
==> τred1't P h (e, xs) (e', xs')"
by(blast intro: tranclp.r_into_trancl)
lemma τred1't_2step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e; ¬ IUF e (ε :: J1_thread_action) e';
P \<turnstile>1 ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove1 P h e'; ¬ IUF e' (ε :: J1_thread_action) e'' |]
==> τred1't P h (e, xs) (e'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τred1't_1step])
lemma τred1't_3step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e; ¬ IUF e (ε :: J1_thread_action) e';
P \<turnstile>1 ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove1 P h e'; ¬ IUF e' (ε :: J1_thread_action) e'';
P \<turnstile>1 ⟨e'', (h, xs'')⟩ -ε-> ⟨e''', (h, xs''')⟩; τmove1 P h e''; ¬ IUF e'' (ε :: J1_thread_action) e''' |]
==> τred1't P h (e, xs) (e''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τred1't_2step])
lemma τreds1't_1step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es; ¬ IUFs es (ε :: J1_thread_action) es' |]
==> τreds1't P h (es, xs) (es', xs')"
by(blast intro: tranclp.r_into_trancl)
lemma τreds1't_2step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es; ¬ IUFs es (ε :: J1_thread_action) es';
P \<turnstile>1 ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves1 P h es'; ¬ IUFs es' (ε :: J1_thread_action) es'' |]
==> τreds1't P h (es, xs) (es'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds1't_1step])
lemma τreds1't_3step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es; ¬ IUFs es (ε :: J1_thread_action) es';
P \<turnstile>1 ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves1 P h es'; ¬ IUFs es' (ε :: J1_thread_action) es'';
P \<turnstile>1 ⟨es'', (h, xs'')⟩ [-ε->] ⟨es''', (h, xs''')⟩; τmoves1 P h es''; ¬ IUFs es'' (ε :: J1_thread_action) es''' |]
==> τreds1't P h (es, xs) (es''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds1't_2step])
lemma τred1'r_1step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e; ¬ IUF e (ε :: J1_thread_action) e' |]
==> τred1'r P h (e, xs) (e', xs')"
by(blast intro: r_into_rtranclp)
lemma τred1'r_2step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e; ¬ IUF e (ε :: J1_thread_action) e';
P \<turnstile>1 ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove1 P h e'; ¬ IUF e' (ε :: J1_thread_action) e'' |]
==> τred1'r P h (e, xs) (e'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred1'r_1step])
lemma τred1'r_3step:
"[| P \<turnstile>1 ⟨e, (h, xs)⟩ -ε-> ⟨e', (h, xs')⟩; τmove1 P h e; ¬ IUF e (ε :: J1_thread_action) e';
P \<turnstile>1 ⟨e', (h, xs')⟩ -ε-> ⟨e'', (h, xs'')⟩; τmove1 P h e'; ¬ IUF e' (ε :: J1_thread_action) e'';
P \<turnstile>1 ⟨e'', (h, xs'')⟩ -ε-> ⟨e''', (h, xs''')⟩; τmove1 P h e''; ¬ IUF e'' (ε :: J1_thread_action) e''' |]
==> τred1'r P h (e, xs) (e''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred1'r_2step])
lemma τreds1'r_1step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es; ¬ IUFs es (ε :: J1_thread_action) es' |]
==> τreds1'r P h (es, xs) (es', xs')"
by(blast intro: r_into_rtranclp)
lemma τreds1'r_2step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es; ¬ IUFs es (ε :: J1_thread_action) es';
P \<turnstile>1 ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves1 P h es'; ¬ IUFs es' (ε :: J1_thread_action) es'' |]
==> τreds1'r P h (es, xs) (es'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds1'r_1step])
lemma τreds1'r_3step:
"[| P \<turnstile>1 ⟨es, (h, xs)⟩ [-ε->] ⟨es', (h, xs')⟩; τmoves1 P h es; ¬ IUFs es (ε :: J1_thread_action) es';
P \<turnstile>1 ⟨es', (h, xs')⟩ [-ε->] ⟨es'', (h, xs'')⟩; τmoves1 P h es'; ¬ IUFs es' (ε :: J1_thread_action) es'';
P \<turnstile>1 ⟨es'', (h, xs'')⟩ [-ε->] ⟨es''', (h, xs''')⟩; τmoves1 P h es''; ¬ IUFs es'' (ε :: J1_thread_action) es''' |]
==> τreds1'r P h (es, xs) (es''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds1'r_2step])
lemma τred1't_preserves_len: "τred1't P h (e, xs) (e', xs') ==> length xs' = length xs"
by(induct rule: tranclp_induct2)(auto dest: red1_preserves_len)
lemma τred1'r_preserves_len: "τred1'r P h (e, xs) (e', xs') ==> length xs' = length xs"
by(induct rule: rtranclp_induct2)(auto dest: red1_preserves_len)
lemma τred1't_inj_τreds1't: "τred1't P h (e, xs) (e', xs') ==> τreds1't P h (e # es, xs) (e' # es, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl List1Red1 τmoves1Hd)
lemma τreds1't_cons_τreds1't: "τreds1't P h (es, xs) (es', xs') ==> τreds1't P h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl List1Red2 τmoves1Tl)
lemma τred1'r_inj_τreds1'r: "τred1'r P h (e, xs) (e', xs') ==> τreds1'r P h (e # es, xs) (e' # es, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl List1Red1 τmoves1Hd)
lemma τreds1'r_cons_τreds1'r: "τreds1'r P h (es, xs) (es', xs') ==> τreds1'r P h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl List1Red2 τmoves1Tl)
lemma NewArray_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl New1ArrayRed τmove1NewArray)
lemma Cast_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Cast1Red τmove1Cast)
lemma BinOp_τred1't_xt1:
"τred1't P h (e1, xs) (e1', xs') ==> τred1't P h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Bin1OpRed1 τmove1BinOp1)
lemma BinOp_τred1't_xt2:
"τred1't P h (e2, xs) (e2', xs') ==> τred1't P h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Bin1OpRed2 τmove1BinOp2)
lemma LAss_τred1't:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (V := e, xs) (V := e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl LAss1Red τmove1LAss)
lemma AAcc_τred1't_xt1:
"τred1't P h (a, xs) (a', xs') ==> τred1't P h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAcc1Red1 τmove1AAcc1)
lemma AAcc_τred1't_xt2:
"τred1't P h (i, xs) (i', xs') ==> τred1't P h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAcc1Red2 τmove1AAcc2)
lemma AAss_τred1't_xt1:
"τred1't P h (a, xs) (a', xs') ==> τred1't P h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAss1Red1 τmove1AAss1)
lemma AAss_τred1't_xt2:
"τred1't P h (i, xs) (i', xs') ==> τred1't P h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAss1Red2 τmove1AAss2)
lemma AAss_τred1't_xt3:
"τred1't P h (e, xs) (e', xs') ==> τred1't 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 AAss1Red3 τmove1AAss3)
lemma ALength_τred1't_xt:
"τred1't P h (a, xs) (a', xs') ==> τred1't P h (a•length, xs) (a'•length, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ALength1Red τmove1ALength)
lemma FAcc_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (e•F{D}, xs) (e'•F{D}, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAcc1Red τmove1FAcc)
lemma FAss_τred1't_xt1:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (e•F{D} := e2, xs) (e'•F{D} := e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAss1Red1 τmove1FAss1)
lemma FAss_τred1't_xt2:
"τred1't P h (e, xs) (e', xs') ==> τred1't 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 FAss1Red2 τmove1FAss2)
lemma Call_τred1't_obj:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (e•M(ps), xs) (e'•M(ps), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Call1Obj τmove1CallObj)
lemma Call_τred1't_param:
"τreds1't P h (es, xs) (es', xs') ==> τred1't P h (Val v•M(es), xs) (Val v•M(es'), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Call1Params τmove1CallParams)
lemma Block_None_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h ({V:T=None; e}, xs) ({V:T=None; e'}, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl τmove1Block elim!: Block1Red)
lemma Block_τred1't_Some:
"[| τred1't P h (e, xs[V := v]) (e', xs'); V < length xs |]
==> τred1't P h ({V:Ty=⌊v⌋; e}, xs) ({V:Ty=None; e'}, xs')"
by(blast intro: tranclp_into_tranclp2 Block1Some τmove1BlockSome Block_None_τred1't_xt)
lemma Sync_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (syncV (e) e2, xs) (syncV (e') e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Synchronized1Red1 τmove1Sync)
lemma InSync_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (insyncV (a) e, xs) (insyncV (a) e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Synchronized1Red2 τmove1InSync)
lemma Seq_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Seq1Red τmove1Seq)
lemma Cond_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't 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 Cond1Red τmove1Cond)
lemma Throw_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't P h (throw e, xs) (throw e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Throw1Red τmove1Throw)
lemma Try_τred1't_xt:
"τred1't P h (e, xs) (e', xs') ==> τred1't 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 Try1Red τmove1Try)
lemma NewArray_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl New1ArrayRed τmove1NewArray)
lemma Cast_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Cast1Red τmove1Cast)
lemma BinOp_τred1'r_xt1:
"τred1'r P h (e1, xs) (e1', xs') ==> τred1'r P h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Bin1OpRed1 τmove1BinOp1)
lemma BinOp_τred1'r_xt2:
"τred1'r P h (e2, xs) (e2', xs') ==> τred1'r P h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Bin1OpRed2 τmove1BinOp2)
lemma LAss_τred1'r:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (V := e, xs) (V := e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl LAss1Red τmove1LAss)
lemma AAcc_τred1'r_xt1:
"τred1'r P h (a, xs) (a', xs') ==> τred1'r P h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAcc1Red1 τmove1AAcc1)
lemma AAcc_τred1'r_xt2:
"τred1'r P h (i, xs) (i', xs') ==> τred1'r P h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAcc1Red2 τmove1AAcc2)
lemma AAss_τred1'r_xt1:
"τred1'r P h (a, xs) (a', xs') ==> τred1'r P h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAss1Red1 τmove1AAss1)
lemma AAss_τred1'r_xt2:
"τred1'r P h (i, xs) (i', xs') ==> τred1'r P h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAss1Red2 τmove1AAss2)
lemma AAss_τred1'r_xt3:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r 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 AAss1Red3 τmove1AAss3)
lemma ALength_τred1'r_xt:
"τred1'r P h (a, xs) (a', xs') ==> τred1'r P h (a•length, xs) (a'•length, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ALength1Red τmove1ALength)
lemma FAcc_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (e•F{D}, xs) (e'•F{D}, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAcc1Red τmove1FAcc)
lemma FAss_τred1'r_xt1:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (e•F{D} := e2, xs) (e'•F{D} := e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAss1Red1 τmove1FAss1)
lemma FAss_τred1'r_xt2:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r 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 FAss1Red2 τmove1FAss2)
lemma Call_τred1'r_obj:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (e•M(ps), xs) (e'•M(ps), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Call1Obj τmove1CallObj)
lemma Call_τred1'r_param:
"τreds1'r P h (es, xs) (es', xs') ==> τred1'r P h (Val v•M(es), xs) (Val v•M(es'), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Call1Params τmove1CallParams)
lemma Block_None_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h ({V:T=None; e}, xs) ({V:T=None; e'}, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl τmove1Block elim!: Block1Red)
lemma Block_τred1'r_Some:
"[| τred1'r P h (e, xs[V := v]) (e', xs'); V < length xs |]
==> τred1'r P h ({V:Ty=⌊v⌋; e}, xs) ({V:Ty=None; e'}, xs')"
by(blast intro: converse_rtranclp_into_rtranclp Block1Some τmove1BlockSome Block_None_τred1'r_xt)
lemma Sync_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (syncV (e) e2, xs) (syncV (e') e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Synchronized1Red1 τmove1Sync)
lemma InSync_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (insyncV (a) e, xs) (insyncV (a) e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Synchronized1Red2 τmove1InSync)
lemma Seq_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Seq1Red τmove1Seq)
lemma Cond_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r 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 Cond1Red τmove1Cond)
lemma Throw_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r P h (throw e, xs) (throw e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Throw1Red τmove1Throw)
lemma Try_τred1'r_xt:
"τred1'r P h (e, xs) (e', xs') ==> τred1'r 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 Try1Red τmove1Try)
lemma τred1't_ThrowD [dest]: "τred1't P h (Throw a, xs) (e'', xs'') ==> e'' = Throw a ∧ xs'' = xs"
by(induct rule: tranclp_induct2)(auto)
lemma τred1'r_ThrowD [dest]: "τred1'r P h (Throw a, xs) (e'', xs'') ==> e'' = Throw a ∧ xs'' = xs"
by(induct rule: rtranclp_induct2)(auto)
definition τRed1' :: "J1_prog => heap => (expr1 × locals1) × ((expr1 × locals1) list) =>
(expr1 × locals1) × ((expr1 × locals1) list) => bool"
where
"τRed1' P h exexs ex'exs' =
(P \<turnstile>1 ⟨fst exexs/snd exexs, h⟩ -ε-> ⟨fst ex'exs'/snd ex'exs', h⟩ ∧ τMove1 P h exexs ∧ ¬ IUFL (fst exexs) (snd exexs) (ε :: J1_thread_action) (fst ex'exs') (snd ex'exs'))"
lemma τRed1'_conv [iff]:
"τRed1' P h (ex, exs) (ex', exs') = (P \<turnstile>1 ⟨ex/exs, h⟩ -ε-> ⟨ex'/exs', h⟩ ∧ τMove1 P h (ex, exs) ∧ ¬ IUFL ex exs (ε :: J1_thread_action) ex' exs')"
by(simp add: τRed1'_def)
abbreviation τRed1't :: "J1_prog => heap => (expr1 × locals1) × ((expr1 × locals1) list) =>
(expr1 × locals1) × ((expr1 × locals1) list) => bool"
where "τRed1't P h ≡ (τRed1' P h)^++"
abbreviation τRed1'r :: "J1_prog => heap => (expr1 × locals1) × ((expr1 × locals1) list) =>
(expr1 × locals1) × ((expr1 × locals1) list) => bool"
where "τRed1'r P h ≡ (τRed1' P h)^**"
lemma τred1't_into_τRed1't:
"τred1't P h (e, xs) (e'', xs'') ==> τRed1't P h ((e, xs), exs) ((e'', xs''), exs)"
by(induct rule: tranclp_induct2)(fastsimp dest: red1Red intro: τmove1Block tranclp.intros simp add: IUFL_def)+
lemma τred1'r_into_τRed1'r:
"τred1'r P h (e, xs) (e'', xs'') ==> τRed1'r P h ((e, xs), exs) ((e'', xs''), exs)"
by(induct rule: rtranclp_induct2)(fastsimp dest: red1Red intro: τmove1Block rtranclp.intros simp add: IUFL_def)+
lemma τred1't_max_vars: "τred1't P h (e, xs) (e', xs') ==> max_vars e' ≤ max_vars e"
by(induct rule: tranclp_induct2)(auto dest: red1_max_vars)
lemma τred1'r_max_vars: "τred1'r P h (e, xs) (e', xs') ==> max_vars e' ≤ max_vars e"
by(induct rule: rtranclp_induct2)(auto dest: red1_max_vars)
abbreviation τMOVE1 :: "'m prog => (((expr1 × locals1) × (expr1 × locals1) list) × heap,
(addr,addr,(expr1 × locals1) × (expr1 × locals1) list,heap,addr, obs_event option) thread_action) trsys"
where "τMOVE1 P ≡ λ(exexs, h) ta s. τMove1 P h exexs ∧ ta = ε"
abbreviation final_expr1 :: "(expr1 × locals1) × (expr1 × locals1) list => bool" where
"final_expr1 ≡ λ(ex, exs). final (fst ex) ∧ exs = []"
lemma Red1'_mthr: "multithreaded (mred1' P)"
apply(unfold_locales)
apply(fastsimp elim!: Red1.cases dest: red1_new_thread_heap)
done
interpretation Red1'_mthr: multithreaded final_expr1 "mred1' P" for P
by(rule Red1'_mthr)
interpretation Red1'_τmthr: τmultithreaded final_expr1 "mred1' P" "τMOVE1 P" for P
by(unfold_locales)
interpretation Red1'_mthr: final_thread_wf final_expr1 "mred1' P" for P
by(unfold_locales)(auto elim!: Red1.cases simp add: final_iff)
lemma red1_τmove1_heap_unchanged: "[| P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩; τmove1 P (hp s) e |] ==> hp s' = hp s"
and red1_τmoves1_heap_unchanged: "[| P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩; τmoves1 P (hp s) es |] ==> hp s' = hp s"
apply(induct rule: red1_reds1.inducts)
apply(fastsimp simp add: map_eq_append_conv)+
done
lemma Red1'_τmthr_wf: "τmultithreaded_wf final_expr1 (mred1' P) (τMOVE1 P) wfs"
proof
fix x1 m1 ta1 x1' m1'
assume "mred1' P (x1, m1) ta1 (x1', m1')" "τMOVE1 P (x1, m1) ta1 (x1', m1')"
thus "m1 = m1'" by(cases x1)(fastsimp elim!: Red1.cases dest: red1_τmove1_heap_unchanged)
next
fix s ta s'
assume "τMOVE1 P s ta s'"
thus "ta = ε" by(simp add: split_beta)
qed
interpretation Red1'_τmthr_wf: τmultithreaded_wf final_expr1 "mred1' P" "τMOVE1 P" wfs for P wfs
by(rule Red1'_τmthr_wf)
lemma Red1_mthr: "multithreaded (mred1 P)"
apply(unfold_locales)
apply(fastsimp elim!: Red1.cases dest: red1_new_thread_heap)
done
interpretation Red1_mthr: multithreaded final_expr1 "mred1 P" for P
by(rule Red1_mthr)
interpretation Red1_τmthr : τmultithreaded final_expr1 "mred1 P" "τMOVE1 P" for P
.
interpretation Red1_mthr: final_thread_wf final_expr1 "mred1 P" for P
by(unfold_locales)(auto elim!: Red1.cases simp add: final_iff)
lemma Red1_τmthr_wf: "τmultithreaded_wf final_expr1 (mred1 P) (τMOVE1 P) wfs"
proof
fix x1 m1 ta1 x1' m1'
assume "mred1 P (x1, m1) ta1 (x1', m1')" "τMOVE1 P (x1, m1) ta1 (x1', m1')"
thus "m1 = m1'" by(cases x1)(fastsimp elim!: Red1.cases dest: red1_τmove1_heap_unchanged)
next
fix s ta s'
assume "τMOVE1 P s ta s'"
thus "ta = ε" by(simp add: split_beta)
qed
interpretation Red'_τmthr_wf: τmultithreaded_wf final_expr1 "mred1 P" "τMOVE1 P" wfs for P wfs
by(rule Red1_τmthr_wf)
end