Theory J1WellType
section ‹Type rules for the intermediate language›
theory J1WellType imports
J1State
"../Common/ExternalCallWF"
"../Common/SemiType"
begin
declare Listn.lesub_list_impl_same_size[simp del] listE_length [simp del]
subsection "Well-Typedness"
type_synonym
env1 = "ty list"
inductive WT1 :: "'addr J1_prog ⇒ env1 ⇒ 'addr expr1 ⇒ ty ⇒ bool" ("_,_ ⊢1 _ :: _" [51,0,0,51] 50)
and WTs1 :: "'addr J1_prog ⇒ env1 ⇒ 'addr expr1 list ⇒ ty list ⇒ bool" ("_,_ ⊢1 _ [::] _" [51,0,0,51]50)
for P :: "'addr J1_prog"
where
WT1New:
"is_class P C ⟹
P,E ⊢1 new C :: Class C"
| WT1NewArray:
"⟦ P,E ⊢1 e :: Integer; is_type P (T⌊⌉) ⟧ ⟹
P,E ⊢1 newA T⌊e⌉ :: T⌊⌉"
| WT1Cast:
"⟦ P,E ⊢1 e :: T; P ⊢ U ≤ T ∨ P ⊢ T ≤ U; is_type P U ⟧
⟹ P,E ⊢1 Cast U e :: U"
| WT1InstanceOf:
"⟦ P,E ⊢1 e :: T; P ⊢ U ≤ T ∨ P ⊢ T ≤ U; is_type P U; is_refT U ⟧
⟹ P,E ⊢1 e instanceof U :: Boolean"
| WT1Val:
"typeof v = Some T ⟹
P,E ⊢1 Val v :: T"
| WT1Var:
"⟦ E!V = T; V < size E ⟧ ⟹
P,E ⊢1 Var V :: T"
| WT1BinOp:
"⟦ P,E ⊢1 e1 :: T1; P,E ⊢1 e2 :: T2; P ⊢ T1«bop»T2 :: T ⟧
⟹ P,E ⊢1 e1«bop»e2 :: T"
| WT1LAss:
"⟦ E!i = T; i < size E; P,E ⊢1 e :: T'; P ⊢ T' ≤ T ⟧
⟹ P,E ⊢1 i:=e :: Void"
| WT1AAcc:
"⟦ P,E ⊢1 a :: T⌊⌉; P,E ⊢1 i :: Integer ⟧
⟹ P,E ⊢1 a⌊i⌉ :: T"
| WT1AAss:
"⟦ P,E ⊢1 a :: T⌊⌉; P,E ⊢1 i :: Integer; P,E ⊢1 e :: T'; P ⊢ T' ≤ T ⟧
⟹ P,E ⊢1 a⌊i⌉ := e :: Void"
| WT1ALength:
"P,E ⊢1 a :: T⌊⌉ ⟹ P,E ⊢1 a∙length :: Integer"
| WTFAcc1:
"⟦ P,E ⊢1 e :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D ⟧
⟹ P,E ⊢1 e∙F{D} :: T"
| WTFAss1:
"⟦ P,E ⊢1 e1 :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D; P,E ⊢1 e2 :: T'; P ⊢ T' ≤ T ⟧
⟹ P,E ⊢1 e1∙F{D} := e2 :: Void"
| WTCAS1:
"⟦ P,E ⊢1 e1 :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D; volatile fm;
P,E ⊢1 e2 :: T'; P ⊢ T' ≤ T; P,E ⊢1 e3 :: T''; P ⊢ T'' ≤ T ⟧
⟹ P,E ⊢1 e1∙compareAndSwap(D∙F, e2, e3) :: Boolean"
| WT1Call:
"⟦ P,E ⊢1 e :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees M:Ts → T = m in D;
P,E ⊢1 es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧
⟹ P,E ⊢1 e∙M(es) :: T"
| WT1Block:
"⟦ is_type P T; P,E@[T] ⊢1 e :: T'; case vo of None ⇒ True | ⌊v⌋ ⇒ ∃T'. typeof v = ⌊T'⌋ ∧ P ⊢ T' ≤ T ⟧
⟹ P,E ⊢1 {V:T=vo; e} :: T'"
| WT1Synchronized:
"⟦ P,E ⊢1 o' :: T; is_refT T; T ≠ NT; P,E@[Class Object] ⊢1 e :: T' ⟧
⟹ P,E ⊢1 sync⇘V⇙ (o') e :: T'"
| WT1Seq:
"⟦ P,E ⊢1 e⇩1::T⇩1; P,E ⊢1 e⇩2::T⇩2 ⟧
⟹ P,E ⊢1 e⇩1;;e⇩2 :: T⇩2"
| WT1Cond:
"⟦ P,E ⊢1 e :: Boolean; P,E ⊢1 e⇩1::T⇩1; P,E ⊢1 e⇩2::T⇩2; P ⊢ lub(T⇩1,T⇩2) = T ⟧
⟹ P,E ⊢1 if (e) e⇩1 else e⇩2 :: T"
| WT1While:
"⟦ P,E ⊢1 e :: Boolean; P,E ⊢1 c::T ⟧
⟹ P,E ⊢1 while (e) c :: Void"
| WT1Throw:
"⟦ P,E ⊢1 e :: Class C; P ⊢ C ≼⇧* Throwable ⟧ ⟹
P,E ⊢1 throw e :: Void"
| WT1Try:
"⟦ P,E ⊢1 e⇩1 :: T; P,E@[Class C] ⊢1 e⇩2 :: T; is_class P C ⟧
⟹ P,E ⊢1 try e⇩1 catch(C V) e⇩2 :: T"
| WT1Nil: "P,E ⊢1 [] [::] []"
| WT1Cons: "⟦ P,E ⊢1 e :: T; P,E ⊢1 es [::] Ts ⟧ ⟹ P,E ⊢1 e#es [::] T#Ts"
declare WT1_WTs1.intros[intro!]
declare WT1Nil[iff]
inductive_cases WT1_WTs1_cases[elim!]:
"P,E ⊢1 Val v :: T"
"P,E ⊢1 Var i :: T"
"P,E ⊢1 Cast D e :: T"
"P,E ⊢1 e instanceof U :: T"
"P,E ⊢1 i:=e :: T"
"P,E ⊢1 {i:U=vo; e} :: T"
"P,E ⊢1 e1;;e2 :: T"
"P,E ⊢1 if (e) e1 else e2 :: T"
"P,E ⊢1 while (e) c :: T"
"P,E ⊢1 throw e :: T"
"P,E ⊢1 try e1 catch(C i) e2 :: T"
"P,E ⊢1 e∙F{D} :: T"
"P,E ⊢1 e1∙F{D}:=e2 :: T"
"P,E ⊢1 e∙compareAndSwap(D∙F, e', e'') :: T"
"P,E ⊢1 e1 «bop» e2 :: T"
"P,E ⊢1 new C :: T"
"P,E ⊢1 newA T'⌊e⌉ :: T"
"P,E ⊢1 a⌊i⌉ := e :: T"
"P,E ⊢1 a⌊i⌉ :: T"
"P,E ⊢1 a∙length :: T"
"P,E ⊢1 e∙M(es) :: T"
"P,E ⊢1 sync⇘V⇙ (o') e :: T"
"P,E ⊢1 insync⇘V⇙ (a) e :: T"
"P,E ⊢1 [] [::] Ts"
"P,E ⊢1 e#es [::] Ts"
lemma WTs1_same_size: "P,E ⊢1 es [::] Ts ⟹ size es = size Ts"
by (induct es arbitrary: Ts) auto
lemma WTs1_snoc_cases:
assumes wt: "P,E ⊢1 es @ [e] [::] Ts"
obtains T Ts' where "P,E ⊢1 es [::] Ts'" "P,E ⊢1 e :: T"
proof -
from wt have "∃T Ts'. P,E ⊢1 es [::] Ts' ∧ P,E ⊢1 e :: T"
by(induct es arbitrary: Ts) auto
thus thesis by(auto intro: that)
qed
lemma WTs1_append:
assumes wt: "P,Env ⊢1 es @ es' [::] Ts"
obtains Ts' Ts'' where "P,Env ⊢1 es [::] Ts'" "P,Env ⊢1 es' [::] Ts''"
proof -
from wt have "∃Ts' Ts''. P,Env ⊢1 es [::] Ts' ∧ P,Env ⊢1 es' [::] Ts''"
by(induct es arbitrary: Ts) auto
thus ?thesis by(auto intro: that)
qed
lemma WT1_not_contains_insync: "P,E ⊢1 e :: T ⟹ ¬ contains_insync e"
and WTs1_not_contains_insyncs: "P,E ⊢1 es [::] Ts ⟹ ¬ contains_insyncs es"
by(induct rule: WT1_WTs1.inducts) auto
lemma WT1_expr_locks: "P,E ⊢1 e :: T ⟹ expr_locks e = (λa. 0)"
and WTs1_expr_lockss: "P,E ⊢1 es [::] Ts ⟹ expr_lockss es = (λa. 0)"
by(induct rule: WT1_WTs1.inducts)(auto)
lemma assumes wf: "wf_prog wfmd P"
shows WT1_unique: "P,E ⊢1 e :: T1 ⟹ P,E ⊢1 e :: T2 ⟹ T1 = T2"
and WTs1_unique: "P,E ⊢1 es [::] Ts1 ⟹ P,E ⊢1 es [::] Ts2 ⟹ Ts1 = Ts2"
apply(induct arbitrary: T2 and Ts2 rule:WT1_WTs1.inducts)
apply blast
apply blast
apply blast
apply blast
apply clarsimp
apply blast
apply(blast dest: WT_binop_fun)
apply blast
apply blast
apply blast
apply blast
apply (blast dest:sees_field_idemp sees_field_fun)
apply (blast dest: sees_field_fun)
apply blast
apply(erule WT1_WTs1_cases)
apply(simp)
apply (blast dest:sees_method_idemp sees_method_fun)
apply blast
apply blast
apply blast
apply(blast dest: is_lub_unique[OF wf])
apply blast
apply blast
apply blast
apply blast
apply blast
done
lemma assumes wf: "wf_prog p P"
shows WT1_is_type: "P,E ⊢1 e :: T ⟹ set E ⊆ types P ⟹ is_type P T"
and WTs1_is_type: "P,E ⊢1 es [::] Ts ⟹ set E ⊆ types P ⟹ set Ts ⊆ types P"
apply(induct rule:WT1_WTs1.inducts)
apply simp
apply simp
apply simp
apply simp
apply (simp add:typeof_lit_is_type)
apply (fastforce intro:nth_mem)
apply(simp add: WT_binop_is_type)
apply(simp)
apply(simp del: is_type_array add: is_type_ArrayD)
apply(simp)
apply(simp)
apply (simp add:sees_field_is_type[OF _ wf])
apply simp
apply simp
apply(fastforce dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
apply(simp)
apply(simp add: is_class_Object[OF wf])
apply simp
apply(blast dest: is_lub_is_type[OF wf])
apply simp
apply simp
apply simp
apply simp
apply(simp)
done
lemma blocks1_WT:
"⟦ P,Env @ Ts ⊢1 body :: T; set Ts ⊆ types P ⟧ ⟹ P,Env ⊢1 blocks1 (length Env) Ts body :: T"
proof(induct n≡"length Env" Ts body arbitrary: Env rule: blocks1.induct)
case 1 thus ?case by simp
next
case (2 T' Ts e)
note IH = ‹⋀Env'. ⟦Suc (length Env) = length Env'; P,Env' @ Ts ⊢1 e :: T; set Ts ⊆ types P ⟧
⟹ P,Env' ⊢1 blocks1 (length Env') Ts e :: T›
from ‹set (T' # Ts) ⊆ types P› have "set Ts ⊆ types P" "is_type P T'" by(auto)
moreover from ‹P,Env @ T' # Ts ⊢1 e :: T› have "P,(Env @ [T']) @ Ts ⊢1 e :: T" by simp
note IH[OF _ this]
ultimately show ?case by auto
qed
lemma WT1_fv: "⟦ P,E ⊢1 e :: T; ℬ e (length E); syncvars e ⟧ ⟹ fv e ⊆ {0..<length E}"
and WTs1_fvs: "⟦ P,E ⊢1 es [::] Ts; ℬs es (length E); syncvarss es ⟧ ⟹ fvs es ⊆ {0..<length E}"
proof(induct rule: WT1_WTs1.inducts)
case (WT1Synchronized E e1 T e2 T' V)
note IH1 = ‹⟦ℬ e1 (length E); syncvars e1⟧ ⟹ fv e1 ⊆ {0..<length E}›
note IH2 = ‹⟦ℬ e2 (length (E @ [Class Object])); syncvars e2⟧ ⟹ fv e2 ⊆ {0..<length (E @ [Class Object])}›
from ‹ℬ (sync⇘V⇙ (e1) e2) (length E)› have [simp]: "V = length E"
and B1: "ℬ e1 (length E)" and B2: "ℬ e2 (Suc (length E))" by auto
from ‹syncvars (sync⇘V⇙ (e1) e2)› have sync1: "syncvars e1" and sync2: "syncvars e2" and V: "V ∉ fv e2" by auto
have "fv e2 ⊆ {0..<length E}"
proof
fix x
assume x: "x ∈ fv e2"
with V have "x ≠ length E" by auto
moreover from IH2 B2 sync2 have "fv e2 ⊆ {0..<Suc (length E)}" by auto
with x have "x < Suc (length E)" by auto
ultimately show "x ∈ {0..<length E}" by auto
qed
with IH1[OF B1 sync1] show ?case by(auto)
next
case (WT1Cond E e e1 T1 e2 T2 T)
thus ?case by(auto del: subsetI)
qed fastforce+
end