# Theory TypeSafe

```(*  Title:      JinjaDCI/J/TypeSafe.thy

Author:     Tobias Nipkow, Susannah Mansky
Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

Based on the Jinja theory J/TypeSafe.thy by Tobias Nipkow
*)

section ‹ Type Safety Proof ›

theory TypeSafe
imports Progress BigStep SmallStep JWellForm
begin

(* here because it requires well-typing def *)
lemma red_shext_incr: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩
⟹ (⋀E T. P,E,h,sh ⊢ e : T ⟹ sh ⊴⇩s sh')"
and reds_shext_incr: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩
⟹ (⋀E Ts. P,E,h,sh ⊢ es [:] Ts ⟹ sh ⊴⇩s sh')"
(*<*)
proof(induct rule:red_reds_inducts) qed(auto simp: shext_def)
(*>*)

lemma wf_types_clinit:
assumes wf:"wf_prog wf_md P" and ex: "class P C = Some a" and proc: "sh C = ⌊(sfs, Processing)⌋"
shows "P,E,h,sh ⊢ C∙⇩sclinit([]) : Void"
proof -
from ex obtain D fs ms where "a = (D,fs,ms)" by(cases a)
then have sP: "(C, D, fs, ms) ∈ set P" using ex map_of_SomeD[of P C a] by(simp add: class_def)
then have "wf_clinit ms" using assms by(unfold wf_prog_def wf_cdecl_def, auto)
then obtain pns body where sm: "(clinit, Static, [], Void, pns, body) ∈ set ms"
by(unfold wf_clinit_def) auto
then have "P ⊢ C sees clinit,Static:[] → Void = (pns,body) in C"
using mdecl_visible[OF wf sP sm] by simp
then show ?thesis using WTrtSCall proc by simp
qed

subsection‹Basic preservation lemmas›

text‹ First some easy preservation lemmas. ›

theorem red_preserves_hconf:
"P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ (⋀T E. ⟦ P,E,h,sh ⊢ e : T; P ⊢ h √ ⟧ ⟹ P ⊢ h' √)"
and reds_preserves_hconf:
"P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ (⋀Ts E. ⟦ P,E,h,sh ⊢ es [:] Ts; P ⊢ h √ ⟧ ⟹ P ⊢ h' √)"
(*<*)
proof (induct rule:red_reds_inducts)
case (RedNew h a C FDTs h' l sh es)
have new: "new_Addr h = Some a" and fields: "P ⊢ C has_fields FDTs"
and h': "h' = h(a↦blank P C)"
and hconf: "P ⊢ h √" by fact+
from new have None: "h a = None" by(rule new_Addr_SomeD)
moreover have "P,h ⊢ blank P C √"
using fields by(rule oconf_blank)
ultimately show "P ⊢ h' √" using h' by(fast intro: hconf_new[OF hconf])
next
case (RedFAss C F t D h a fs v l sh b')
let ?fs' = "fs((F,D)↦v)"
have hconf: "P ⊢ h √" and ha: "h a = Some(C,fs)"
and wt: "P,E,h,sh ⊢ addr a∙F{D}:=Val v : T" by fact+
from wt ha obtain TF Tv where typeofv: "typeof⇘h⇙ v = Some Tv"
and has: "P ⊢ C has F,NonStatic:TF in D"
and sub: "P ⊢ Tv ≤ TF" by auto
have "P,h ⊢ (C, ?fs') √"
proof (rule oconf_fupd[OF has])
show "P,h ⊢ (C, fs) √" using hconf ha by(simp add:hconf_def)
show "P,h ⊢ v :≤ TF" using sub typeofv by(simp add:conf_def)
qed
with hconf ha show "P ⊢ h(a↦(C, ?fs')) √"  by (rule hconf_upd_obj)
qed(auto elim: WTrt.cases)
(*>*)

theorem red_preserves_lconf:
"P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹
(⋀T E. ⟦ P,E,h,sh ⊢ e:T; P,h ⊢ l (:≤) E ⟧ ⟹ P,h' ⊢ l' (:≤) E)"
and reds_preserves_lconf:
"P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹
(⋀Ts E. ⟦ P,E,h,sh ⊢ es[:]Ts; P,h ⊢ l (:≤) E ⟧ ⟹ P,h' ⊢ l' (:≤) E)"
(*<*)
proof(induct rule:red_reds_inducts)
case RedNew thus ?case
by(fast intro:lconf_hext red_hext_incr[OF red_reds.RedNew])
next
case RedLAss thus ?case by(fastforce elim: lconf_upd simp:conf_def)
next
case RedFAss thus ?case
by(fast intro:lconf_hext red_hext_incr[OF red_reds.RedFAss])
next
case (InitBlockRed e h l V v sh b e' h' l' sh' b' v' T T')
have red: "P ⊢ ⟨e, (h, l(V↦v),sh),b⟩ → ⟨e',(h', l',sh'),b'⟩"
and IH: "⋀T E . ⟦ P,E,h,sh ⊢ e:T; P,h ⊢ l(V↦v) (:≤) E ⟧
⟹ P,h' ⊢ l' (:≤) E"
and l'V: "l' V = Some v'" and lconf: "P,h ⊢ l (:≤) E"
and wt: "P,E,h,sh ⊢ {V:T := Val v; e} : T'" by fact+
from lconf_hext[OF lconf red_hext_incr[OF red]]
have "P,h' ⊢ l (:≤) E" .
moreover from IH lconf wt have "P,h' ⊢ l' (:≤) E(V↦T)"
by(auto simp del: fun_upd_apply simp: fun_upd_same lconf_upd2 conf_def)
ultimately show "P,h' ⊢ l'(V := l V) (:≤) E"
by (fastforce simp:lconf_def split:if_split_asm)
next
case (BlockRedNone e h l V sh b e' h' l' sh' b' T T')
have red: "P ⊢ ⟨e,(h, l(V := None),sh),b⟩ → ⟨e',(h', l',sh'),b'⟩"
and IH: "⋀E T. ⟦ P,E,h,sh ⊢ e : T; P,h ⊢ l(V:=None) (:≤) E ⟧
⟹ P,h' ⊢ l' (:≤) E"
and lconf: "P,h ⊢ l (:≤) E" and wt: "P,E,h,sh ⊢ {V:T; e} : T'" by fact+
from lconf_hext[OF lconf red_hext_incr[OF red]]
have "P,h' ⊢ l (:≤) E" .
moreover have "P,h' ⊢ l' (:≤) E(V↦T)"
by(rule IH, insert lconf wt, auto simp:lconf_def)
ultimately show "P,h' ⊢ l'(V := l V) (:≤) E"
by (fastforce simp:lconf_def split:if_split_asm)
next
case (BlockRedSome e h l V sh b e' h' l' sh' b' v T T')
have red: "P ⊢ ⟨e,(h, l(V := None),sh),b⟩ → ⟨e',(h', l',sh'),b'⟩"
and IH: "⋀E T. ⟦P,E,h,sh ⊢ e : T; P,h ⊢ l(V:=None) (:≤) E⟧
⟹ P,h' ⊢ l' (:≤) E"
and lconf: "P,h ⊢ l (:≤) E" and wt: "P,E,h,sh ⊢ {V:T; e} : T'" by fact+
from lconf_hext[OF lconf red_hext_incr[OF red]]
have "P,h' ⊢ l (:≤) E" .
moreover have "P,h' ⊢ l' (:≤) E(V↦T)"
by(rule IH, insert lconf wt, auto simp:lconf_def)
ultimately show "P,h' ⊢ l'(V := l V) (:≤) E"
by (fastforce simp:lconf_def split:if_split_asm)
qed(auto elim: WTrt.cases)
(*>*)

theorem red_preserves_shconf:
"P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ (⋀T E. ⟦ P,E,h,sh ⊢ e : T; P,h ⊢⇩s sh √ ⟧ ⟹ P,h' ⊢⇩s sh' √)"
and reds_preserves_shconf:
"P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ (⋀Ts E. ⟦ P,E,h,sh ⊢ es [:] Ts; P,h ⊢⇩s sh √ ⟧ ⟹ P,h' ⊢⇩s sh' √)"
(*<*)
proof (induct rule:red_reds_inducts)
case (RedNew h a C FDTs h' l sh es)
have new: "new_Addr h = Some a"
and h': "h' = h(a↦blank P C)"
and shconf: "P,h ⊢⇩s sh √" by fact+
from new have None: "h a = None" by(rule new_Addr_SomeD)
then show "P,h' ⊢⇩s sh √" using h' by(fast intro: shconf_hnew[OF shconf])
next
case (RedFAss C F t D h a fs v l sh b)
let ?fs' = "fs((F,D)↦v)"
have shconf: "P,h ⊢⇩s sh √" and ha: "h a = Some(C,fs)" by fact+
then show "P,h(a↦(C, ?fs')) ⊢⇩s sh √" by (rule shconf_hupd_obj)
next
case (RedSFAss C F t D sh sfs i sfs' v sh' h l)
let ?sfs' = "sfs(F↦v)"
have shconf: "P,h ⊢⇩s sh √" and shD: "sh D = ⌊(sfs, i)⌋"
and wt: "P,E,h,sh ⊢ C∙⇩sF{D} := Val v : T" by fact+
from wt obtain TF Tv where typeofv: "typeof⇘h⇙ v = Some Tv"
and has: "P ⊢ C has F,Static:TF in D"
and sub: "P ⊢ Tv ≤ TF" by (auto elim: WTrt.cases)
have has': "P ⊢ D has F,Static:TF in D" using has by(rule has_field_idemp)
have "P,h,D ⊢⇩s ?sfs' √"
proof (rule soconf_fupd[OF has'])
show "P,h,D ⊢⇩s sfs √" using shconf shD by(simp add:shconf_def)
show "P,h ⊢ v :≤ TF" using sub typeofv by(simp add:conf_def)
qed
with shconf have "P,h ⊢⇩s sh(D↦(?sfs',i)) √" by (rule shconf_upd_obj)
then show ?case using RedSFAss.hyps(3) RedSFAss.hyps(4) by blast
next
case (InitNoneRed sh C C' Cs e h l)
let ?sfs' = "sblank P C"
have "P,h ⊢⇩s sh(C ↦ (?sfs', Prepared)) √"
proof(rule shconf_upd_obj)
show "P,h ⊢⇩s sh √" using InitNoneRed by simp
show "P,h,C ⊢⇩s sblank P C √" by (metis has_field_def soconf_def soconf_sblank)
qed
then show ?case by blast
next
case (InitObjectRed sh C sfs sh' C' Cs e h l)
have sh': "sh' = sh(C ↦ (sfs, Processing))" by fact
have "P,h ⊢⇩s sh(C ↦ (sfs, Processing)) √"
proof(rule shconf_upd_obj)
show "P,h ⊢⇩s sh √" using InitObjectRed by simp
moreover have "sh C = ⌊(sfs, Prepared)⌋" using InitObjectRed by simp
ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
qed
then show ?case using sh' by blast
next
case (InitNonObjectSuperRed sh C sfs D a b sh' C' Cs e h l)
have sh': "sh' = sh(C ↦ (sfs, Processing))" by fact
have "P,h ⊢⇩s sh(C ↦ (sfs, Processing)) √"
proof(rule shconf_upd_obj)
show "P,h ⊢⇩s sh √" using InitNonObjectSuperRed by simp
moreover have "sh C = ⌊(sfs, Prepared)⌋" using InitNonObjectSuperRed by simp
ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
qed
then show ?case using sh' by blast
next
case (RedRInit sh C sfs i sh' C' Cs e v h l)
have sh': "sh' = sh(C ↦ (sfs, Done))" by fact
have "P,h ⊢⇩s sh(C ↦ (sfs, Done)) √"
proof(rule shconf_upd_obj)
show "P,h ⊢⇩s sh √" using RedRInit by simp
moreover have "sh C = ⌊(sfs, i)⌋" using RedRInit by simp
ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
qed
then show ?case using sh' by blast
next
case (RInitInitThrow sh C sfs i sh' a D Cs e h l)
have sh': "sh' = sh(C ↦ (sfs, Error))" by fact
have "P,h ⊢⇩s sh(C ↦ (sfs, Error)) √"
proof(rule shconf_upd_obj)
show "P,h ⊢⇩s sh √" using RInitInitThrow by simp
moreover have "sh C = ⌊(sfs, i)⌋" using RInitInitThrow by simp
ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
qed
then show ?case using sh' by blast
next
case (RInitThrow sh C sfs i sh' a e' h l)
have sh': "sh' = sh(C ↦ (sfs, Error))" by fact
have "P,h ⊢⇩s sh(C ↦ (sfs, Error)) √"
proof(rule shconf_upd_obj)
show "P,h ⊢⇩s sh √" using RInitThrow by simp
moreover have "sh C = ⌊(sfs, i)⌋" using RInitThrow by simp
ultimately show "P,h,C ⊢⇩s sfs √" using shconfD by blast
qed
then show ?case using sh' by blast
qed(auto elim: WTrt.cases)
(*>*)

theorem assumes wf: "wwf_J_prog P"
shows red_preserves_iconf:
"P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ iconf sh e ⟹ iconf sh' e'"
and reds_preserves_iconf:
"P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ iconfs sh es ⟹ iconfs sh' es'"
(*<*)
proof (induct rule:red_reds_inducts)
case (BinOpRed1 e h l sh b e' h' l' sh' b' bop e⇩2)
then show ?case using BinOpRed1 nsub_RI_iconf[of e⇩2 sh'] val_of_spec
proof(cases "val_of e") qed(simp,fast)
next
case (FAssRed1 e h l sh b e' h' l' sh' b' F D e⇩2)
then show ?case using FAssRed1 nsub_RI_iconf[of e⇩2 sh'] val_of_spec
proof(cases "val_of e") qed(simp,fast)
next
case (CallObj e h l sh b e' h' l' sh' b' M es)
then show ?case using CallObj nsub_RIs_iconfs[of es sh'] val_of_spec
proof(cases "val_of e") qed(simp,fast)
next
case RedCall then show ?case using sees_wwf_nsub_RI[OF wf RedCall.hyps(2)]
by (clarsimp simp: assigned_def nsub_RI_iconf)
next
case (RedSCall C M Ts T pns body D vs a a b)
then have "¬sub_RI (blocks (pns, Ts, vs, body))"
using sees_wwf_nsub_RI[OF wf RedSCall.hyps(1)] by simp
then show ?case by(rule nsub_RI_iconf)
next
case SCallInitRed then show ?case by fastforce
next
case (BlockRedNone e h l V sh b e' h' l' sh' b' T)
then show ?case by auto
next
case (SeqRed e h l sh b e' h' l' sh' b' e⇩2)
then show ?case
proof(cases "lass_val_of e")
case None then show ?thesis using SeqRed nsub_RI_iconf by(auto dest: val_of_spec)
next
case (Some a)
have "e' = unit ∧ sh' = sh" by(simp add: lass_val_of_red[OF Some SeqRed(1)])
then show ?thesis using SeqRed Some by(auto dest: val_of_spec)
qed
next
case (ListRed1 e h l sh b e' h' l' sh' b' es)
then show ?case using ListRed1 nsub_RIs_iconfs[of es sh'] val_of_spec
proof(cases "val_of e") qed(simp,fast)
next
case RedInit then show ?case by(auto simp: nsub_RI_iconf)
next
case (RedInitDone sh C sfs C' Cs e h l b)
then show ?case proof(cases Cs) qed(auto simp: initPD_def)
next
case (RedInitProcessing sh C sfs C' Cs e h l b)
then show ?case proof(cases Cs) qed(auto simp: initPD_def)
next
case (RedRInit sh C sfs i sh' C' Cs v e h l b)
then show ?case proof(cases Cs) qed(auto simp: initPD_def)
next
case CallThrowParams then show ?case by(auto simp: iconfs_map_throw)
next
case SCallThrowParams then show ?case by(auto simp: iconfs_map_throw)
qed(auto simp: nsub_RI_iconf lass_val_of_iconf)
(*>*)

lemma Seq_bconf_preserve_aux:
assumes "P ⊢ ⟨e,(h, l, sh),b⟩ → ⟨e',(h', l', sh'),b'⟩" and "P,sh ⊢⇩b (e;; e⇩2,b) √"
and "P,sh ⊢⇩b (e::expr,b) √ ⟶ P,sh' ⊢⇩b (e'::expr,b') √"
shows "P,sh' ⊢⇩b (e';;e⇩2,b') √"
proof(cases "val_of e")
case None show ?thesis
proof(cases "lass_val_of e")
case lNone: None show ?thesis
proof(cases "lass_val_of e'")
case lNone': None
then show ?thesis using None assms lNone
by(auto dest: val_of_spec simp: bconf_def option.distinct(1))
next
case (Some a)
then show ?thesis using None assms lNone by(auto dest: lass_val_of_spec simp: bconf_def)
qed
next
case (Some a)
then show ?thesis using None assms by(auto dest: lass_val_of_spec)
qed
next
case (Some a)
then show ?thesis using assms by(auto dest: val_of_spec)
qed

theorem red_preserves_bconf:
"P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ iconf sh e ⟹ P,sh ⊢⇩b (e,b) √ ⟹ P,sh' ⊢⇩b (e',b') √"
and reds_preserves_bconf:
"P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ iconfs sh es ⟹ P,sh ⊢⇩b (es,b) √ ⟹ P,sh' ⊢⇩b (es',b') √"
(*<*)
proof (induct rule:red_reds_inducts)
case (CastRed e a a b b e' a a b b' C) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (BinOpRed1 e h l sh b e' h' l' sh' b' bop e⇩2) show ?case
proof(cases b')
case True with BinOpRed1 val_of_spec show ?thesis
proof(cases "val_of e") qed(simp,fast)
next
case False then show ?thesis by (simp add: bconf_def)
qed
next
case (BinOpRed2 e a a b b e' a a b b' v⇩1 bop) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (LAssRed e a a b b e' a a b b' V) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (FAccRed e a a b b e' a a b b' F D) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (RedSFAccNonStatic C F t D h l sh b) then show ?case
using has_field_fun[of P C F NonStatic] by (auto simp: bconf_def)
next
case (FAssRed1 e h l sh b e' h' l' sh' b' F D e⇩2) show ?case
proof(cases b')
case True with FAssRed1 val_of_spec show ?thesis
proof(cases "val_of e'")qed((simp,fast)+)
next
case False then show ?thesis by(simp add: bconf_def)
qed
next
case (FAssRed2 e a a b b e' a a b b' v F D) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (SFAssRed e h l sh b e' h' l' sh' b' C F D) then show ?case
proof(cases b') qed(fastforce simp: bconf_def val_no_step)+
next
case (RedSFAssNonStatic C F t D v a a b b) then show ?case
using has_field_fun[of P C F NonStatic] by (auto simp: bconf_def)
next
case (CallObj e h l sh b e' h' l' sh' b' M es) show ?case
proof(cases b')
case True with CallObj val_of_spec show ?thesis
proof(cases "val_of e'")qed((simp,fast)+)
next
case False then show ?thesis by(simp add: bconf_def)
qed
next
case (CallParams es a a b b es' a a b b' v M) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (SCallParams es h l sh b es' h' l' sh' b' C M) show ?case
proof(cases b')
case b': True show ?thesis
proof(cases "map_vals_of es'")
case None
then show ?thesis using SCallParams b' vals_no_step
proof(cases "map_vals_of es")qed(clarsimp,fast)
next
case f: Some
then show ?thesis using SCallParams b' vals_no_step
proof(cases "map_vals_of es")qed(clarsimp,fast)
qed
next
case False then show ?thesis by(simp add: bconf_def)
qed
next
case (SCallInitDoneRed C M Ts T pns body D sh sfs vs h l)
then show ?case by(auto simp: bconf_def initPD_def) (rule_tac x=D in exI, auto)+
next
case (RedSCallNonStatic C M Ts T a b D vs h l sh b) then show ?case
using sees_method_fun[of P C M NonStatic] by (auto simp: bconf_def)
next
case (BlockRedNone e h l V sh b e' h' l' sh' b' T) show ?case
proof(cases "assigned V e'")
case True
then obtain v e2 where "e' = V := Val v;;e2" by(clarsimp simp: assigned_def)
then show ?thesis using BlockRedNone by(clarsimp simp: bconf_def)
next
case False then show ?thesis using BlockRedNone by simp
qed
next
case (BlockRedSome e h l V sh b e' h' l' sh' b' v T) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (InitBlockRed e h l V v sh b e' h' l' sh' b' v' T) show ?case
proof(cases b')
case True
then show ?thesis using InitBlockRed by (simp add: assigned_def)
next
case False then show ?thesis by(simp add: bconf_def)
qed
next
case (RedBlock V T u)
then have "¬assigned V (Val u)" by(clarsimp simp: assigned_def)
then show ?case using RedBlock by(simp add: bconf_def)
next
case (SeqRed e h l sh b e' h' l' sh' b' e⇩2)
have "iconf sh e"
proof(cases "lass_val_of e")
case (Some a) show ?thesis by(rule lass_val_of_iconf[OF Some])
next
case None then show ?thesis using SeqRed by(auto dest: val_of_spec)
qed
then show ?case using SeqRed Seq_bconf_preserve_aux by simp
next
case (CondRed e a a b b e' a a b b' e⇩1 e⇩2) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (ThrowRed e a a b b e' a a b b') then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (TryRed e a a b b e' a a b b' C V e⇩2) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (ListRed1 e h l sh b e' h' l' sh' b' es)
with val_of_spec show ?case
next
case (RedInit C b' e X Y b b'')
then show ?case
by(auto simp: bconf_def icheck_ss_exp icheck_init_class icheck_curr_init)
next
case (RInitRed e a a b b e' a a b b' C Cs e⇩0) then show ?case
proof(cases b') qed(simp, simp add: bconf_def)
next
case (BlockThrow V T a)
then have "¬assigned V (Throw a)" by(simp add: assigned_def)
then show ?case using BlockThrow by simp
qed(simp_all, auto simp: bconf_def initPD_def)
(*>*)

text‹ Preservation of definite assignment more complex and requires a
few lemmas first. ›

lemma [iff]: "⋀A. ⟦ length Vs = length Ts; length vs = length Ts⟧ ⟹
𝒟 (blocks (Vs,Ts,vs,e)) A = 𝒟 e (A ⊔ ⌊set Vs⌋)"
(*<*)
by (induct Vs Ts vs e rule:blocks_induct)
(*>*)

lemma red_lA_incr: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩
⟹ ⌊dom l⌋ ⊔ 𝒜 e ⊑  ⌊dom l'⌋ ⊔ 𝒜 e'"
and reds_lA_incr: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩
⟹ ⌊dom l⌋ ⊔ 𝒜s es ⊑  ⌊dom l'⌋ ⊔ 𝒜s es'"
(*<*)
proof(induct rule:red_reds_inducts)
case TryRed then show ?case
(blast dest:red_lcl_incr)+
next
case BinOpRed1 then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case BinOpRed2 then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case LAssRed then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case FAssRed1 then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case FAssRed2 then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case CallObj then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case CallParams then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case BlockRedNone then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case BlockRedSome then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case InitBlockRed then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case SeqRed then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case CondRed then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case RedCondT then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case RedCondF then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case ListRed1 then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
next
case ListRed2 then show ?case
by(auto simp del:fun_upd_apply simp:hyperset_defs)
(*>*)

text‹ Now preservation of definite assignment. ›

lemma assumes wf: "wf_J_prog P"
shows red_preserves_defass:
"P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ 𝒟 e ⌊dom l⌋ ⟹ 𝒟 e' ⌊dom l'⌋"
and "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ 𝒟s es ⌊dom l⌋ ⟹ 𝒟s es' ⌊dom l'⌋"
(*<*)
proof (induct rule:red_reds_inducts)
case BinOpRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
case FAssRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
case CallObj thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
next
case RedCall thus ?case
by (auto dest!:sees_wf_mdecl[OF wf] simp:wf_mdecl_def hyperset_defs elim!:D_mono')
next
case RedSCall thus ?case
by (auto dest!:sees_wf_mdecl[OF wf] simp:wf_mdecl_def hyperset_defs elim!:D_mono')
next
case SCallInitRed
then show ?case by(auto simp:hyperset_defs Ds_Vals)
next
case InitBlockRed thus ?case
by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
case BlockRedNone thus ?case
by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
case BlockRedSome thus ?case
by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
case SeqRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
case CondRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
case TryRed thus ?case
by (fastforce dest:red_lcl_incr intro:D_mono' simp:hyperset_defs)
next
case ListRed1 thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
next
case RedWhile thus ?case by(auto simp:hyperset_defs elim!:D_mono')
next
case RedInit then show ?case by (auto intro: D_mono' simp: hyperset_defs)
next
case (RInitRed e h l sh b e' h' l' sh' b' C Cs e⇩0)
then show ?case by(auto simp:hyperset_defs dest:red_lcl_incr elim!:D_mono')
qed(auto simp:hyperset_defs)
(*>*)

text‹ Combining conformance of heap, static heap, and local variables: ›

definition sconf :: "J_prog ⇒ env ⇒ state ⇒ bool"   ("_,_ ⊢ _ √"   [51,51,51]50)
where
"P,E ⊢ s √  ≡  let (h,l,sh) = s in P ⊢ h √ ∧ P,h ⊢ l (:≤) E ∧ P,h ⊢⇩s sh √"

lemma red_preserves_sconf:
"⟦ P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩; P,E,hp s,shp s ⊢ e : T; P,E ⊢ s √ ⟧ ⟹ P,E ⊢ s' √"
(*<*)
by(fastforce intro:red_preserves_hconf red_preserves_lconf red_preserves_shconf
(*>*)

lemma reds_preserves_sconf:
"⟦ P ⊢ ⟨es,s,b⟩ [→] ⟨es',s',b'⟩; P,E,hp s,shp s ⊢ es [:] Ts; P,E ⊢ s √ ⟧ ⟹ P,E ⊢ s' √"
(*<*)
by(fastforce intro:reds_preserves_hconf reds_preserves_lconf reds_preserves_shconf
(*>*)

subsection "Subject reduction"

lemma wt_blocks:
"⋀E. ⟦ length Vs = length Ts; length vs = length Ts ⟧ ⟹
(P,E,h,sh ⊢ blocks(Vs,Ts,vs,e) : T) =
(P,E(Vs[↦]Ts),h,sh ⊢ e:T ∧ (∃Ts'. map (typeof⇘h⇙) vs = map Some Ts' ∧ P ⊢ Ts' [≤] Ts))"
(*<*)
proof(induct Vs Ts vs e rule:blocks_induct)
case (1 V Vs T Ts v vs e)
then show ?case by(force simp add:rel_list_all2_Cons2)
qed simp_all
(*>*)

theorem assumes wf: "wf_J_prog P"
shows subject_reduction2: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹
(⋀E T. ⟦ P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e:T ⟧
⟹ ∃T'. P,E,h',sh' ⊢ e':T' ∧ P ⊢ T' ≤ T)"
and subjects_reduction2: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹
(⋀E Ts. ⟦ P,E ⊢ (h,l,sh) √; iconfs sh es; P,E,h,sh ⊢ es [:] Ts ⟧
⟹ ∃Ts'. P,E,h',sh' ⊢ es' [:] Ts' ∧ P ⊢ Ts' [≤] Ts)"
(*<*)
proof (induct rule:red_reds_inducts)
case RedNew then show ?case by (auto simp: blank_def)
next
case RedNewFail thus ?case
by (unfold sconf_def hconf_def) (fastforce elim!:typeof_OutOfMemory)
next
case CastRed thus ?case
by(clarsimp simp:is_refT_def)
(blast intro: widens_trans dest!:widen_Class[THEN iffD1])
next
case RedCastFail thus ?case
by (unfold sconf_def hconf_def)  (fastforce elim!:typeof_ClassCast)
next
case (BinOpRed1 e⇩1 h l sh b e⇩1' h' l' sh' b' bop e⇩2)
have red: "P ⊢ ⟨e⇩1,(h,l,sh),b⟩ → ⟨e⇩1',(h',l',sh'),b'⟩"
and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e⇩1; P,E,h,sh ⊢ e⇩1:T⟧
⟹ ∃U. P,E,h',sh' ⊢ e⇩1' : U ∧ P ⊢ U ≤ T"
and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (e⇩1 «bop» e⇩2)"
and wt: "P,E,h,sh ⊢ e⇩1 «bop» e⇩2 : T" by fact+
have val: "val_of e⇩1 = None" using red iconf val_no_step by auto
then have iconf1: "iconf sh e⇩1" and nsub_RI2: "¬sub_RI e⇩2" using iconf by simp+
have "P,E,h',sh' ⊢ e⇩1' «bop» e⇩2 : T"
proof (cases bop)
assume [simp]: "bop = Eq"
from wt obtain T⇩1 T⇩2 where [simp]: "T = Boolean"
and wt⇩1: "P,E,h,sh ⊢ e⇩1 : T⇩1" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : T⇩2" by auto
show ?thesis
using WTrt_hext_shext_mono[OF wt⇩2 red_hext_incr[OF red] red_shext_incr[OF red wt⇩1] nsub_RI2]
IH[OF conf iconf1 wt⇩1] by auto
next
from wt have [simp]: "T = Integer"
and wt⇩1: "P,E,h,sh ⊢ e⇩1 : Integer" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : Integer"
by auto
show ?thesis
using WTrt_hext_shext_mono[OF wt⇩2 red_hext_incr[OF red] red_shext_incr[OF red wt⇩1] nsub_RI2]
IH[OF conf iconf1 wt⇩1] by auto
qed
thus ?case by auto
next
case (BinOpRed2 e⇩2 h l sh b e⇩2' h' l' sh' b' v⇩1 bop)
have red: "P ⊢ ⟨e⇩2,(h,l,sh),b⟩ → ⟨e⇩2',(h',l',sh'),b'⟩"
and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e⇩2; P,E,h,sh ⊢ e⇩2:T⟧
⟹ ∃U. P,E,h',sh' ⊢ e⇩2' : U ∧ P ⊢ U ≤ T"
and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (Val v⇩1 «bop» e⇩2)"
and wt: "P,E,h,sh ⊢ (Val v⇩1) «bop» e⇩2 : T" by fact+
have iconf2: "iconf sh e⇩2" using iconf by simp
have "P,E,h',sh' ⊢ (Val v⇩1) «bop» e⇩2' : T"
proof (cases bop)
assume [simp]: "bop = Eq"
from wt obtain T⇩1 T⇩2 where [simp]: "T = Boolean"
and wt⇩1: "P,E,h,sh ⊢ Val v⇩1 : T⇩1" and wt⇩2: "P,E,h,sh ⊢ e⇩2:T⇩2" by auto
show ?thesis
using IH[OF conf iconf2 wt⇩2] WTrt_hext_mono[OF wt⇩1 red_hext_incr[OF red]]
by auto
next
from wt have [simp]: "T = Integer"
and wt⇩1: "P,E,h,sh ⊢ Val v⇩1 : Integer" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : Integer"
by auto
show ?thesis
using IH[OF conf iconf2 wt⇩2] WTrt_hext_mono[OF wt⇩1 red_hext_incr[OF red]]
by auto
qed
thus ?case by auto
next
case (RedBinOp bop) thus ?case
proof (cases bop)
case Eq thus ?thesis using RedBinOp by auto
next
case Add thus ?thesis using RedBinOp by auto
qed
next
case RedVar thus ?case by (fastforce simp:sconf_def lconf_def conf_def)
next
case (LAssRed e h l sh b e' h' l' sh' b' V)
obtain Te where Te: "P,E,h,sh ⊢ e : Te ∧ P ⊢ Te ≤ the(E V)" using LAssRed.prems(3) by auto
then have wide: "P ⊢ Te ≤ the(E V)" using LAssRed by simp
then have "∃T'. P,E,h',sh' ⊢ e' : T' ∧ P ⊢ T' ≤ Te"
using LAssRed.hyps(2) LAssRed.prems(1,2) Te widen_trans[OF _ wide] by auto
then obtain T' where wt: "P,E,h',sh' ⊢ e' : T' ∧ P ⊢ T' ≤ Te" by clarsimp
have "P,E,h',sh' ⊢ V:=e' : Void" using LAssRed wt widen_trans[OF _ wide] by auto
then show ?case using LAssRed by(rule_tac x = Void in exI) auto
next
case (FAccRed e h l sh b e' h' l' sh' b' F D)
have IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (e∙F{D})"
and wt: "P,E,h,sh ⊢ e∙F{D} : T" by fact+
have iconf': "iconf sh e" using iconf by simp+
― ‹The goal: ?case = @{prop ?case}›
― ‹Now distinguish the two cases how wt can have arisen.›
{ fix C assume wte: "P,E,h,sh ⊢ e : Class C"
and has: "P ⊢ C has F,NonStatic:T in D"
from IH[OF conf iconf' wte]
obtain U where wte': "P,E,h',sh' ⊢ e' : U" and UsubC: "P ⊢ U ≤ Class C"
by auto
― ‹Now distinguish what @{term U} can be.›
{ assume "U = NT" hence ?case using wte'
by(blast intro:WTrtFAccNT widen_refl) }
moreover
{ fix C' assume U: "U = Class C'" and C'subC: "P ⊢ C' ≼⇧* C"
from has_field_mono[OF has C'subC] wte' U
have ?case by(blast intro:WTrtFAcc) }
ultimately have ?case using UsubC by(simp add: widen_Class) blast }
moreover
{ assume "P,E,h,sh ⊢ e : NT"
hence "P,E,h',sh' ⊢ e' : NT" using IH[OF conf iconf'] by fastforce
hence ?case  by(fastforce intro:WTrtFAccNT widen_refl) }
ultimately show ?case using wt by blast
next
case RedFAcc thus ?case
by(fastforce simp:sconf_def hconf_def oconf_def conf_def has_field_def
dest:has_fields_fun)
next
case RedFAccNull thus ?case
by(fastforce intro: widen_refl WTThrow[OF WTVal] elim!: typeof_NullPointer
simp: sconf_def hconf_def)
next
case RedSFAccNone then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_NoSuchFieldError
simp: sconf_def hconf_def)
next
case RedFAccStatic then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
simp: sconf_def hconf_def)
next
case (RedSFAcc C F t D sh sfs i v h l es)
then have "P ⊢ C has F,Static:T in D" by fast
then have dM: "P ⊢ D has F,Static:T in D" by(rule has_field_idemp)
then show ?case using RedSFAcc by(fastforce simp:sconf_def shconf_def soconf_def conf_def)
next
case SFAccInitDoneRed then show ?case by (meson widen_refl)
next
case (SFAccInitRed C F t D sh h l E T)
have "is_class P D" using SFAccInitRed.hyps(1) by(rule has_field_is_class')
then have "P,E,h,sh ⊢ INIT D ([D],False) ← C∙⇩sF{D} : T ∧ P ⊢ T ≤ T"
using SFAccInitRed WTrtInit[OF SFAccInitRed.prems(3)] by clarsimp
then show ?case by(rule exI)
next
case RedSFAccNonStatic then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
simp: sconf_def hconf_def)
next
case (FAssRed1 e h l sh b e' h' l' sh' b' F D e⇩2)
have red: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩"
and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (e∙F{D} := e⇩2)"
and wt: "P,E,h,sh ⊢ e∙F{D}:=e⇩2 : T" by fact+
have val: "val_of e = None" using red iconf val_no_step by auto
then have iconf': "iconf sh e" and nsub_RI2: "¬sub_RI e⇩2" using iconf by simp+
from wt have void: "T = Void" by blast
― ‹We distinguish if @{term e} has type @{term NT} or a Class type›
― ‹Remember ?case = @{term ?case}›
{ assume wt':"P,E,h,sh ⊢ e : NT"
hence "P,E,h',sh' ⊢ e' : NT" using IH[OF conf iconf'] by fastforce
moreover obtain T⇩2 where "P,E,h,sh ⊢ e⇩2 : T⇩2" using wt by auto
from this red_hext_incr[OF red] red_shext_incr[OF red wt'] nsub_RI2 have  "P,E,h',sh' ⊢ e⇩2 : T⇩2"
by(rule WTrt_hext_shext_mono)
ultimately have ?case using void by(blast intro!:WTrtFAssNT)
}
moreover
{ fix C TF T⇩2 assume wt⇩1: "P,E,h,sh ⊢ e : Class C" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : T⇩2"
and has: "P ⊢ C has F,NonStatic:TF in D" and sub: "P ⊢ T⇩2 ≤ TF"
obtain U where wt⇩1': "P,E,h',sh' ⊢ e' : U" and UsubC: "P ⊢ U ≤ Class C"
using IH[OF conf iconf' wt⇩1] by blast
have wt⇩2': "P,E,h',sh' ⊢ e⇩2 : T⇩2"
by(rule WTrt_hext_shext_mono[OF wt⇩2 red_hext_incr[OF red] red_shext_incr[OF red wt⇩1] nsub_RI2])
― ‹Is @{term U} the null type or a class type?›
{ assume "U = NT" with wt⇩1' wt⇩2' void have ?case
by(blast intro!:WTrtFAssNT) }
moreover
{ fix C' assume UClass: "U = Class C'" and "subclass": "P ⊢ C' ≼⇧* C"
have "P,E,h',sh' ⊢ e' : Class C'" using wt⇩1' UClass by auto
moreover have "P ⊢ C' has F,NonStatic:TF in D"
by(rule has_field_mono[OF has "subclass"])
ultimately have ?case using wt⇩2' sub void by(blast intro:WTrtFAss) }
ultimately have ?case using UsubC by(auto simp add:widen_Class) }
ultimately show ?case using wt by blast
next
case (FAssRed2 e⇩2 h l sh b e⇩2' h' l' sh' b' v F D)
have red: "P ⊢ ⟨e⇩2,(h,l,sh),b⟩ → ⟨e⇩2',(h',l',sh'),b'⟩"
and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e⇩2; P,E,h,sh ⊢ e⇩2 : T⟧
⟹ ∃U. P,E,h',sh' ⊢ e⇩2' : U ∧ P ⊢ U ≤ T"
and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (Val v∙F{D} := e⇩2)"
and wt: "P,E,h,sh ⊢ Val v∙F{D}:=e⇩2 : T" by fact+
have iconf2: "iconf sh e⇩2" using iconf by simp
from wt have [simp]: "T = Void" by auto
from wt show ?case
proof (rule WTrt_elim_cases)
fix C TF T⇩2
assume wt⇩1: "P,E,h,sh ⊢ Val v : Class C"
and has: "P ⊢ C has F,NonStatic:TF in D"
and wt⇩2: "P,E,h,sh ⊢ e⇩2 : T⇩2" and TsubTF: "P ⊢ T⇩2 ≤ TF"
have wt⇩1': "P,E,h',sh' ⊢ Val v : Class C"
using WTrt_hext_mono[OF wt⇩1 red_hext_incr[OF red]] by auto
obtain T⇩2' where wt⇩2': "P,E,h',sh' ⊢ e⇩2' : T⇩2'" and T'subT: "P ⊢ T⇩2' ≤ T⇩2"
using IH[OF conf iconf2 wt⇩2] by blast
have "P,E,h',sh' ⊢ Val v∙F{D}:=e⇩2' : Void"
by(rule WTrtFAss[OF wt⇩1' has wt⇩2' widen_trans[OF T'subT TsubTF]])
thus ?case by auto
next
fix T⇩2 assume null: "P,E,h,sh ⊢ Val v : NT" and wt⇩2: "P,E,h,sh ⊢ e⇩2 : T⇩2"
from null have "v = Null" by simp
moreover
obtain T⇩2' where "P,E,h',sh' ⊢ e⇩2' : T⇩2' ∧ P ⊢ T⇩2' ≤ T⇩2"
using IH[OF conf iconf2 wt⇩2] by blast
ultimately show ?thesis by(fastforce intro:WTrtFAssNT)
qed
next
case RedFAss thus ?case by(auto simp del:fun_upd_apply)
next
case RedFAssNull thus ?case
by(fastforce intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp:sconf_def hconf_def)
next
case RedFAssStatic then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
simp: sconf_def hconf_def)
next
case (SFAssRed e h l sh b e' h' l' sh' b' C F D E T)
have IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (C∙⇩sF{D} := e)"
and wt: "P,E,h,sh ⊢ C∙⇩sF{D}:=e : T" by fact+
have iconf': "iconf sh e" using iconf by simp
from wt have [simp]: "T = Void" by auto
from wt show ?case
proof (rule WTrt_elim_cases)
fix TF T1
assume has: "P ⊢ C has F,Static:TF in D"
and wt1: "P,E,h,sh ⊢ e : T1" and TsubTF: "P ⊢ T1 ≤ TF"
obtain T' where wt1': "P,E,h',sh' ⊢ e' : T'" and T'subT: "P ⊢ T' ≤ T1"
using IH[OF conf iconf' wt1] by blast
have "P,E,h',sh' ⊢ C∙⇩sF{D}:=e' : Void"
by(rule WTrtSFAss[OF wt1' has widen_trans[OF T'subT TsubTF]])
thus ?case by auto
qed
next
case SFAssInitDoneRed then show ?case by (meson widen_refl)
next
case (SFAssInitRed C F t D sh v h l E T)
have "is_class P D" using SFAssInitRed.hyps(1) by(rule has_field_is_class')
then have "P,E,h,sh ⊢ INIT D ([D],False) ← C∙⇩sF{D} := Val v : T ∧ P ⊢ T ≤ T"
using SFAssInitRed WTrtInit[OF SFAssInitRed.prems(3)] by clarsimp
then show ?case by(rule exI)
next
case RedSFAssNone then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_NoSuchFieldError
simp: sconf_def hconf_def)
next
case RedSFAssNonStatic then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
simp: sconf_def hconf_def)
next
case (CallObj e h l sh b e' h' l' sh' b' M es)
have red: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩"
and IH: "⋀E T. ⟦P,E ⊢ (h,l,sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (e∙M(es))"
and wt: "P,E,h,sh ⊢ e∙M(es) : T" by fact+
have val: "val_of e = None" using red iconf val_no_step by auto
then have iconf': "iconf sh e" and nsub_RIs: "¬sub_RIs es" using iconf by simp+
― ‹We distinguish if @{term e} has type @{term NT} or a Class type›
― ‹Remember ?case = @{term ?case}›
{ assume wt':"P,E,h,sh ⊢ e:NT"
hence "P,E,h',sh' ⊢ e' : NT" using IH[OF conf iconf'] by fastforce
moreover
fix Ts assume wtes: "P,E,h,sh ⊢ es [:] Ts"
have "P,E,h',sh' ⊢ es [:] Ts"
by(rule WTrts_hext_shext_mono[OF wtes red_hext_incr[OF red] red_shext_incr[OF red wt'] nsub_RIs])
ultimately have ?case by(blast intro!:WTrtCallNT) }
moreover
{ fix C D Ts Us pns body
assume wte: "P,E,h,sh ⊢ e : Class C"
and "method": "P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in D"
and wtes: "P,E,h,sh ⊢ es [:] Us" and subs: "P ⊢ Us [≤] Ts"
obtain U where wte': "P,E,h',sh' ⊢ e' : U" and UsubC: "P ⊢ U ≤ Class C"
using IH[OF conf iconf' wte] by blast
― ‹Is @{term U} the null type or a class type?›
{ assume "U = NT"
moreover have "P,E,h',sh' ⊢ es [:] Us"
by(rule WTrts_hext_shext_mono[OF wtes red_hext_incr[OF red] red_shext_incr[OF red wte] nsub_RIs])
ultimately have ?case using wte' by(blast intro!:WTrtCallNT) }
moreover
{ fix C' assume UClass: "U = Class C'" and "subclass": "P ⊢ C' ≼⇧* C"
have "P,E,h',sh' ⊢ e' : Class C'" using wte' UClass by auto
moreover obtain Ts' T' pns' body' D'
where method': "P ⊢ C' sees M,NonStatic:Ts'→T' = (pns',body') in D'"
and subs': "P ⊢ Ts [≤] Ts'" and sub': "P ⊢ T' ≤ T"
using Call_lemma[OF "method" "subclass" wf] by fast
moreover have "P,E,h',sh' ⊢ es [:] Us"
by(rule WTrts_hext_shext_mono[OF wtes red_hext_incr[OF red] red_shext_incr[OF red wte] nsub_RIs])
ultimately have ?case
using subs by(blast intro:WTrtCall rtrancl_trans widens_trans) }
ultimately have ?case using UsubC by(auto simp add:widen_Class) }
ultimately show ?case using wt by auto
next
case (CallParams es h l sh b es' h' l' sh' b' v M)
have reds: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩"
and IH: "⋀E Ts. ⟦P,E ⊢ (h,l,sh) √; iconfs sh es; P,E,h,sh ⊢ es [:] Ts⟧
⟹ ∃Us. P,E,h',sh' ⊢ es' [:] Us ∧ P ⊢ Us [≤] Ts"
and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (Val v∙M(es))"
and wt: "P,E,h,sh ⊢ Val v∙M(es) : T" by fact+
have iconfs: "iconfs sh es" using iconf by simp
from wt show ?case
proof (rule WTrt_elim_cases)
fix C D Ts Us pns body
assume wte: "P,E,h,sh ⊢ Val v : Class C"
and "P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in D"
and wtes: "P,E,h,sh ⊢ es [:] Us" and "P ⊢ Us [≤] Ts"
moreover have "P,E,h',sh' ⊢ Val v : Class C"
using WTrt_hext_mono[OF wte reds_hext_incr[OF reds]] by auto
moreover
obtain Us' where "P,E,h',sh' ⊢ es' [:] Us' ∧ P ⊢ Us' [≤] Us"
using IH[OF conf iconfs wtes] by blast
ultimately show ?thesis by(blast intro:WTrtCall widens_trans)
next
fix Us
assume null: "P,E,h,sh ⊢ Val v : NT" and wtes: "P,E,h,sh ⊢ es [:] Us"
from null have "v = Null" by simp
moreover
obtain Us' where "P,E,h',sh' ⊢ es' [:] Us' ∧ P ⊢ Us' [≤] Us"
using IH[OF conf iconfs wtes] by blast
ultimately show ?thesis by(fastforce intro:WTrtCallNT)
qed
next
case (RedCall h a C fs M Ts T pns body D vs l sh b E T')
have hp: "h a = Some(C,fs)"
and "method": "P ⊢ C sees M,NonStatic: Ts→T = (pns,body) in D"
and wt: "P,E,h,sh ⊢ addr a∙M(map Val vs) : T'" by fact+
obtain Ts' where wtes: "P,E,h,sh ⊢ map Val vs [:] Ts'"
and subs: "P ⊢ Ts' [≤] Ts" and T'isT: "T' = T"
using wt "method" hp by (auto dest:sees_method_fun)
from wtes subs have length_vs: "length vs = length Ts"
by(fastforce simp:list_all2_iff dest!:WTrts_same_length)
from sees_wf_mdecl[OF wf "method"] obtain T''
where wtabody: "P,[this#pns [↦] Class D#Ts] ⊢ body :: T''"
and T''subT: "P ⊢ T'' ≤ T" and length_pns: "length pns = length Ts"
by(fastforce simp:wf_mdecl_def simp del:map_upds_twist)
from wtabody have "P,Map.empty(this#pns [↦] Class D#Ts),h,sh ⊢ body : T''"
by(rule WT_implies_WTrt)
hence "P,E(this#pns [↦] Class D#Ts),h,sh ⊢ body : T''"
by(rule WTrt_env_mono) simp
hence "P,E,h,sh ⊢ blocks(this#pns, Class D#Ts, Addr a#vs, body) : T''"
using wtes subs hp sees_method_decl_above[OF "method"] length_vs length_pns
with T''subT T'isT show ?case by blast
next
case RedCallNull thus ?case
by(fastforce intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp: sconf_def hconf_def)
next
case RedCallStatic then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
simp: sconf_def hconf_def)
next
case (SCallParams es h l sh b es' h' l' sh' b' C M)
have IH: "⋀E Ts. ⟦P,E ⊢ (h,l,sh) √; iconfs sh es; P,E,h,sh ⊢ es [:] Ts⟧
⟹ ∃Us. P,E,h',sh' ⊢ es' [:] Us ∧ P ⊢ Us [≤] Ts"
and conf: "P,E ⊢ (h,l,sh) √" and iconf: "iconf sh (C∙⇩sM(es))"
and wt: "P,E,h,sh ⊢ C∙⇩sM(es) : T" by fact+
have iconfs: "iconfs sh es" using iconf by simp
from wt show ?case
proof (rule WTrt_elim_cases)
fix D Ts Us pns body sfs vs
assume method: "P ⊢ C sees M,Static:Ts→T = (pns,body) in D"
and wtes: "P,E,h,sh ⊢ es [:] Us" and us: "P ⊢ Us [≤] Ts"
and clinit: "M = clinit ⟶ sh D = ⌊(sfs,Processing)⌋ ∧ es = map Val vs"
obtain Us' where es': "P,E,h',sh' ⊢ es' [:] Us'" and us': "P ⊢ Us' [≤] Us"
using IH[OF conf iconfs wtes] by blast
show ?thesis
proof(cases "M = clinit")
case True then show ?thesis using clinit SCallParams.hyps(1) by blast
next
case False
then show ?thesis using es' method us us' by(blast intro:WTrtSCall widens_trans)
qed
qed
next
case (RedSCall C M Ts T pns body D vs h l sh E T')
have "method": "P ⊢ C sees M,Static: Ts→T = (pns,body) in D"
and wt: "P,E,h,sh ⊢ C∙⇩sM(map Val vs) : T'" by fact+
obtain Ts' where wtes: "P,E,h,sh ⊢ map Val vs [:] Ts'"
and subs: "P ⊢ Ts' [≤] Ts" and T'isT: "T' = T"
using wt "method" map_Val_eq by(auto dest:sees_method_fun)+
from wtes subs have length_vs: "length vs = length Ts"
by(fastforce simp:list_all2_iff dest!:WTrts_same_length)
from sees_wf_mdecl[OF wf "method"] obtain T''
where wtabody: "P,[pns [↦] Ts] ⊢ body :: T''"
and T''subT: "P ⊢ T'' ≤ T" and length_pns: "length pns = length Ts"
by(fastforce simp:wf_mdecl_def simp del:map_upds_twist)
from wtabody have "P,Map.empty(pns [↦] Ts),h,sh ⊢ body : T''"
by(rule WT_implies_WTrt)
hence "P,E(pns [↦] Ts),h,sh ⊢ body : T''"
by(rule WTrt_env_mono) simp
hence "P,E,h,sh ⊢ blocks(pns, Ts, vs, body) : T''"
using wtes subs sees_method_decl_above[OF "method"] length_vs length_pns
with T''subT T'isT show ?case by blast
next
case SCallInitDoneRed then show ?case by (meson widen_refl)
next
case (SCallInitRed C F Ts t pns body D sh v h l E T)
have "is_class P D" using SCallInitRed.hyps(1) by(rule sees_method_is_class')
then have "P,E,h,sh ⊢ INIT D ([D],False) ← C∙⇩sF(map Val v) : T ∧ P ⊢ T ≤ T"
using SCallInitRed WTrtInit[OF SCallInitRed.prems(3)] by clarsimp
then show ?case by(rule exI)
next
case RedSCallNone then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_NoSuchMethodError
simp: sconf_def hconf_def)
next
case RedSCallNonStatic then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_IncompatibleClassChangeError
simp: sconf_def hconf_def)
next
case BlockRedNone thus ?case
by(auto simp del:fun_upd_apply)(fastforce simp:sconf_def lconf_def)
next
case (BlockRedSome e h l V sh b e' h' l' sh' b' v T E Te)
have red: "P ⊢ ⟨e,(h,l(V:=None),sh),b⟩ → ⟨e',(h',l',sh'),b'⟩"
and IH: "⋀E T. ⟦P,E ⊢ (h,l(V:=None),sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
⟹ ∃T'. P,E,h',sh' ⊢ e' : T' ∧ P ⊢ T' ≤ T"
and Some: "l' V = Some v" and conf: "P,E ⊢ (h,l,sh) √"
and iconf: "iconf sh {V:T; e}"
and wt: "P,E,h,sh ⊢ {V:T; e} : Te" by fact+
obtain Te' where IH': "P,E(V↦T),h',sh' ⊢ e' : Te' ∧ P ⊢ Te' ≤ Te"
using IH conf iconf wt by(fastforce simp:sconf_def lconf_def)
have "P,h' ⊢ l' (:≤) E(V↦T)" using conf wt
by(fastforce intro:red_preserves_lconf[OF red] simp:sconf_def lconf_def)
hence "P,h' ⊢ v :≤ T" using Some by(fastforce simp:lconf_def)
with IH' show ?case
by(fastforce simp:sconf_def conf_def fun_upd_same simp del:fun_upd_apply)
next
case (InitBlockRed e h l V v sh b e' h' l' sh' b' v' T E T')
have red: "P ⊢ ⟨e, (h,l(V↦v),sh),b⟩ → ⟨e',(h',l',sh'),b'⟩"
and IH: "⋀E T. ⟦P,E ⊢ (h,l(V↦v),sh) √; iconf sh e; P,E,h,sh ⊢ e : T⟧
⟹ ∃U. P,E,h',sh' ⊢ e' : U ∧ P ⊢ U ≤ T"
and v': "l' V = Some v'" and conf: "P,E ⊢ (h,l,sh) √"
and iconf: "iconf sh {V:T; V:=Val v;; e}"
and wt: "P,E,h,sh ⊢ {V:T := Val v; e} : T'" by fact+
from wt obtain T⇩1 where wt⇩1: "typeof⇘h⇙ v = Some T⇩1"
and T1subT: "P ⊢ T⇩1 ≤ T" and wt⇩2: "P,E(V↦T),h,sh ⊢ e : T'" by auto
have lconf⇩2: "P,h ⊢ l(V↦v) (:≤) E(V↦T)" using conf wt⇩1 T1subT
have "∃T⇩1'. typeof⇘h'⇙ v' = Some T⇩1' ∧ P ⊢ T⇩1' ≤ T"
using v' red_preserves_lconf[OF red wt⇩2 lconf⇩2]
by(fastforce simp:lconf_def conf_def)
with IH conf iconf lconf⇩2 wt⇩2 show ?case by (fastforce simp add:sconf_def)
next
case (SeqRed e h l sh b e' h' l' sh' b' e⇩2)
then have val: "val_of e = None" by (simp add: val_no_step)
show ?case
proof(cases "lass_val_of e")
case None
then show ?thesis
using SeqRed val by(auto elim: WTrt_hext_shext_mono[OF _ red_hext_incr red_shext_incr])
next
case (Some a)
have "sh = sh'" using SeqRed lass_val_of_spec[OF Some] by auto
then show ?thesis using SeqRed val Some
by(auto intro: lass_val_of_iconf[OF Some] elim: WTrt_hext_mono[OF _ red_hext_incr])
qed
next
case CondRed thus ?case
by auto (blast intro:WTrt_hext_shext_mono[OF _ red_hext_incr red_shext_incr])+
next
case ThrowRed thus ?case
by(auto simp:is_refT_def)(blast dest:widen_Class[THEN iffD1])+
next
case RedThrowNull thus ?case
by(fastforce intro: WTThrow[OF WTVal] elim!:typeof_NullPointer simp:sconf_def hconf_def)
next
case TryRed thus ?case
by auto (blast intro:widen_trans WTrt_hext_shext_mono[OF _ red_hext_incr red_shext_incr])
next
case RedTryFail thus ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] simp:sconf_def hconf_def)
next
case (ListRed1 e h l sh b e' h' l' sh' b' es)
then have val: "val_of e = None" by(simp add: val_no_step)
obtain U Us where Ts: "Ts = U # Us" using ListRed1 by auto
then have nsub_RI: "¬ sub_RIs es" and wts: "P,E,h,sh ⊢ es [:] Us" and wt: "P,E,h,sh ⊢ e : U"
and IH: "⋀E T. ⟦P,E ⊢ (h, l, sh) √; P,E,h,sh ⊢ e : T⟧ ⟹ ∃T'. P,E,h',sh' ⊢ e' : T' ∧ P ⊢ T' ≤ T"
using ListRed1 val by auto
obtain T' where
"∀E0 E1. (∃T2. P,E1,h',sh' ⊢ e' : T2 ∧ P ⊢ T2 ≤ E0) = (P,E1,h',sh' ⊢ e' : T' E0 E1 ∧ P ⊢ T' E0 E1 ≤ E0)"
by moura
then have disj: "∀E t. ¬ P,E ⊢ (h, l, sh) √ ∨ ¬ P,E,h,sh ⊢ e : t ∨ P,E,h',sh' ⊢ e' : T' t E ∧ P ⊢ T' t E ≤ t"
using IH by presburger
have "P,E,h',sh' ⊢ es [:] Us"
using nsub_RI wts wt by (metis (no_types) ListRed1.hyps(1) WTrts_hext_shext_mono red_hext_incr red_shext_incr)
then have "∃ts. (∃t tsa. ts = t # tsa ∧ P,E,h',sh' ⊢ e' : t ∧ P,E,h',sh' ⊢ es [:] tsa) ∧ P ⊢ ts [≤] (U # Us)"
using disj wt ListRed1.prems(1) by blast
then show ?case using Ts by auto
next
case ListRed2 thus ?case
by(fastforce dest: hext_typeof_mono[OF reds_hext_incr])
next
case (InitNoneRed sh C C' Cs e h l b)
then have sh: "sh ⊴⇩s sh(C ↦ (sblank P C, Prepared))" by(simp add: shext_def)
have wt: "P,E,h,sh(C ↦ (sblank P C, Prepared)) ⊢ INIT C' (C # Cs,False) ← e : T"
using InitNoneRed WTrt_shext_mono[OF _ sh] by fastforce
then show ?case by(rule_tac x = T in exI) (simp add: fun_upd_def)
next
case (RedInitDone sh C sfs C' Cs e h l b)
then have "P,E,h,sh ⊢ INIT C' (Cs,True) ← e : T" by auto (metis Nil_tl list.set_sel(2))
then show ?case by(rule_tac x = T in exI) simp
next
case (RedInitProcessing sh C sfs C' Cs e h l b)
then have "P,E,h,sh ⊢ INIT C' (Cs,True) ← e : T" by auto (metis Nil_tl list.set_sel(2))+
then show ?case by(rule_tac x = T in exI) simp
next
case RedInitError then show ?case
by(fastforce intro: WTrtThrow[OF WTrtVal] elim!: typeof_NoClassDefFoundError
simp: sconf_def hconf_def)
next
case (InitObjectRed sh C sfs sh' C' Cs e h l b)
then have sh: "sh ⊴⇩s sh(Object ↦ (sfs, Processing))" by(simp add: shext_def)
have "P,E,h,sh' ⊢ INIT C' (C # Cs,True) ← e : T"
using InitObjectRed WTrt_shext_mono[OF _ sh] by auto
then show ?case by(rule_tac x = T in exI) (simp add: fun_upd_def)
next
case (InitNonObjectSuperRed sh C sfs D fs ms sh' C' Cs e h l b)
then have sh: "sh ⊴⇩s sh(C ↦ (sfs, Processing))" by(simp add: shext_def)
then have cd: "is_class P D" using InitNonObjectSuperRed class_wf wf wf_cdecl_supD by blast
have sup': "supercls_lst P (C # Cs)" using InitNonObjectSuperRed.prems(3) by auto
then have sup: "supercls_lst P (D # C # Cs)"
using supercls_lst_app[of P C Cs D] subcls1I[OF InitNonObjectSuperRed.hyps(3,2)] by auto
have "distinct (C # Cs)" using InitNonObjectSuperRed.prems(3) by auto
then have dist: "distinct (D # C # Cs)"
using wf_supercls_distinct_app[OF wf InitNonObjectSuperRed.hyps(2-3) sup'] by simp
have "P,E,h,sh' ⊢ INIT C' (D # C # Cs,False) ← e : T"
using InitNonObjectSuperRed WTrt_shext_mono[OF _ sh] cd sup dist by auto
then show ?case by(rule_tac x = T in exI) simp
next
case (RedInitRInit C' C Cs e' h l sh b E T)
then obtain a sfs where C: "class P C = ⌊a⌋" and proc: "sh C = ⌊(sfs, Processing)⌋"
using WTrtInit by(auto simp: is_class_def)
then have T': "P,E,h,sh ⊢ C∙⇩sclinit([]) : Void" using wf_types_clinit[OF wf C] by simp
have "P,E,h,sh ⊢ RI (C,C∙⇩sclinit(<```