# Theory WellType

```(*  Title:      JinjaThreads/J/WellType.thy
Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Well-typedness of Jinja expressions›

theory WellType
imports
Expr
State
"../Common/ExternalCallWF"
"../Common/WellForm"
"../Common/SemiType"
begin

declare Listn.lesub_list_impl_same_size[simp del]
declare listE_length [simp del]

type_synonym
env  = "vname ⇀ ty"

inductive
WT :: "(ty ⇒ ty ⇒ ty ⇒ bool) ⇒ 'addr J_prog ⇒ env ⇒ 'addr expr ⇒ ty ⇒ bool" ("_,_,_ ⊢ _ :: _"   [51,51,51,51]50)
and WTs :: "(ty ⇒ ty ⇒ ty ⇒ bool) ⇒ 'addr J_prog ⇒ env ⇒ 'addr expr list ⇒ ty list ⇒ bool"
("_,_,_ ⊢ _ [::] _"   [51,51,51,51]50)
for is_lub :: "ty ⇒ ty ⇒ ty ⇒ bool" ("⊢ lub'((_,/ _)') = _" [51,51,51] 50)
where

WTNew:
"is_class P C  ⟹
is_lub,P,E ⊢ new C :: Class C"

| WTNewArray:
"⟦ is_lub,P,E ⊢ e :: Integer; is_type P (T⌊⌉) ⟧ ⟹
is_lub,P,E ⊢ newA T⌊e⌉ :: T⌊⌉"

| WTCast:
"⟦ is_lub,P,E ⊢ e :: T; P ⊢ U ≤ T ∨ P ⊢ T ≤ U; is_type P U ⟧
⟹ is_lub,P,E ⊢ Cast U e :: U"

| WTInstanceOf:
"⟦ is_lub,P,E ⊢ e :: T; P ⊢ U ≤ T ∨ P ⊢ T ≤ U; is_type P U; is_refT U ⟧
⟹ is_lub,P,E ⊢ e instanceof U :: Boolean"

| WTVal:
"typeof v = Some T ⟹
is_lub,P,E ⊢ Val v :: T"

| WTVar:
"E V = Some T ⟹
is_lub,P,E ⊢ Var V :: T"

| WTBinOp:
"⟦ is_lub,P,E ⊢ e1 :: T1; is_lub,P,E ⊢ e2 :: T2; P ⊢ T1«bop»T2 :: T ⟧
⟹ is_lub,P,E ⊢ e1«bop»e2 :: T"

| WTLAss:
"⟦ E V = Some T;  is_lub,P,E ⊢ e :: T';  P ⊢ T' ≤ T;  V ≠ this ⟧
⟹ is_lub,P,E ⊢ V:=e :: Void"

| WTAAcc:
"⟦ is_lub,P,E ⊢ a :: T⌊⌉; is_lub,P,E ⊢ i :: Integer ⟧
⟹ is_lub,P,E ⊢ a⌊i⌉ :: T"

| WTAAss:
"⟦ is_lub,P,E ⊢ a :: T⌊⌉; is_lub,P,E ⊢ i :: Integer; is_lub,P,E ⊢ e :: T'; P ⊢ T' ≤ T ⟧
⟹ is_lub,P,E ⊢ a⌊i⌉ := e :: Void"

| WTALength:
"is_lub,P,E ⊢ a :: T⌊⌉ ⟹ is_lub,P,E ⊢ a∙length :: Integer"

| WTFAcc:
"⟦ is_lub,P,E ⊢ e :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D ⟧
⟹ is_lub,P,E ⊢ e∙F{D} :: T"

| WTFAss:
"⟦ is_lub,P,E ⊢ e⇩1 :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D; is_lub,P,E ⊢ e⇩2 :: T'; P ⊢ T' ≤ T ⟧
⟹ is_lub,P,E ⊢ e⇩1∙F{D}:=e⇩2 :: Void"

| WTCAS:
"⟦ is_lub,P,E ⊢ e1 :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees F:T (fm) in D; volatile fm;
is_lub,P,E ⊢ e2 :: T'; P ⊢ T' ≤ T; is_lub,P,E ⊢ e3 :: T''; P ⊢ T'' ≤ T ⟧
⟹  is_lub,P,E ⊢ e1∙compareAndSwap(D∙F, e2, e3) :: Boolean"

| WTCall:
"⟦ is_lub,P,E ⊢ e :: U; class_type_of' U = ⌊C⌋; P ⊢ C sees M:Ts → T = meth in D;
is_lub,P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts ⟧
⟹ is_lub,P,E ⊢ e∙M(es) :: T"

| WTBlock:
"⟦ is_type P T;  is_lub,P,E(V ↦ T) ⊢ e :: T'; case vo of None ⇒ True | ⌊v⌋ ⇒ ∃T'. typeof v = ⌊T'⌋ ∧ P ⊢ T' ≤ T ⟧
⟹  is_lub,P,E ⊢ {V:T=vo; e} :: T'"

| WTSynchronized:
"⟦ is_lub,P,E ⊢ o' :: T; is_refT T; T ≠ NT; is_lub,P,E ⊢ e :: T' ⟧
⟹ is_lub,P,E ⊢ sync(o') e :: T'"

― ‹Note that insync is not statically typable.›

| WTSeq:
"⟦ is_lub,P,E ⊢ e⇩1::T⇩1;  is_lub,P,E ⊢ e⇩2::T⇩2 ⟧
⟹  is_lub,P,E ⊢ e⇩1;;e⇩2 :: T⇩2"

| WTCond:
"⟦ is_lub,P,E ⊢ e :: Boolean;  is_lub,P,E ⊢ e⇩1::T⇩1;  is_lub,P,E ⊢ e⇩2::T⇩2; ⊢ lub(T⇩1, T⇩2) = T ⟧
⟹ is_lub,P,E ⊢ if (e) e⇩1 else e⇩2 :: T"

| WTWhile:
"⟦ is_lub,P,E ⊢ e :: Boolean;  is_lub,P,E ⊢ c::T ⟧
⟹ is_lub,P,E ⊢ while (e) c :: Void"

| WTThrow:
"⟦ is_lub,P,E ⊢ e :: Class C; P ⊢ C ≼⇧* Throwable ⟧ ⟹
is_lub,P,E ⊢ throw e :: Void"

| WTTry:
"⟦ is_lub,P,E ⊢ e⇩1 :: T;  is_lub,P,E(V ↦ Class C) ⊢ e⇩2 :: T; P ⊢ C ≼⇧* Throwable ⟧
⟹ is_lub,P,E ⊢ try e⇩1 catch(C V) e⇩2 :: T"

| WTNil: "is_lub,P,E ⊢ [] [::] []"

| WTCons: "⟦ is_lub,P,E ⊢ e :: T; is_lub,P,E ⊢ es [::] Ts ⟧ ⟹ is_lub,P,E ⊢ e#es [::] T#Ts"

abbreviation WT' :: "'addr J_prog ⇒ env ⇒ 'addr expr ⇒ ty ⇒ bool" ("_,_ ⊢ _ :: _" [51,51,51] 50)
where "WT' P ≡ WT (TypeRel.is_lub P) P"

abbreviation WTs' :: "'addr J_prog ⇒ env ⇒ 'addr expr list ⇒ ty list ⇒ bool" ("_,_ ⊢ _ [::] _" [51,51,51] 50)
where "WTs' P ≡ WTs (TypeRel.is_lub P) P"

declare WT_WTs.intros[intro!]

inductive_simps WTs_iffs [iff]:
"is_lub',P,E ⊢ [] [::] Ts"
"is_lub',P,E ⊢ e#es [::] T#Ts"
"is_lub',P,E ⊢ e#es [::] Ts"

lemma WTs_conv_list_all2:
fixes is_lub
shows "is_lub,P,E ⊢ es [::] Ts = list_all2 (WT is_lub P E) es Ts"
by(induct es arbitrary: Ts)(auto simp add: list_all2_Cons1 elim: WTs.cases)

lemma WTs_append [iff]: "⋀is_lub Ts. (is_lub,P,E ⊢ es⇩1 @ es⇩2 [::] Ts) =
(∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧ is_lub,P,E ⊢ es⇩1 [::] Ts⇩1 ∧ is_lub,P,E ⊢ es⇩2[::]Ts⇩2)"
by(auto simp add: WTs_conv_list_all2 list_all2_append1 dest: list_all2_lengthD[symmetric])

inductive_simps WT_iffs [iff]:
"is_lub',P,E ⊢ Val v :: T"
"is_lub',P,E ⊢ Var V :: T"
"is_lub',P,E ⊢ e⇩1;;e⇩2 :: T⇩2"
"is_lub',P,E ⊢ {V:T=vo; e} :: T'"

inductive_cases WT_elim_cases[elim!]:
"is_lub',P,E ⊢ V :=e :: T"
"is_lub',P,E ⊢ sync(o') e :: T"
"is_lub',P,E ⊢ if (e) e⇩1 else e⇩2 :: T"
"is_lub',P,E ⊢ while (e) c :: T"
"is_lub',P,E ⊢ throw e :: T"
"is_lub',P,E ⊢ try e⇩1 catch(C V) e⇩2 :: T"
"is_lub',P,E ⊢ Cast D e :: T"
"is_lub',P,E ⊢ e instanceof U :: T"
"is_lub',P,E ⊢ a∙F{D} :: T"
"is_lub',P,E ⊢ a∙F{D} := v :: T"
"is_lub',P,E ⊢ e∙compareAndSwap(D∙F, e', e'') :: T"
"is_lub',P,E ⊢ e⇩1 «bop» e⇩2 :: T"
"is_lub',P,E ⊢ new C :: T"
"is_lub',P,E ⊢ newA T⌊e⌉ :: T'"
"is_lub',P,E ⊢ a⌊i⌉ := e :: T"
"is_lub',P,E ⊢ a⌊i⌉ :: T"
"is_lub',P,E ⊢ a∙length :: T"
"is_lub',P,E ⊢ e∙M(ps) :: T"
"is_lub',P,E ⊢ sync(o') e :: T"
"is_lub',P,E ⊢ insync(a) e :: T"

lemma fixes is_lub :: "ty ⇒ ty ⇒ ty ⇒ bool" ("⊢ lub'((_,/ _)') = _" [51,51,51] 50)
assumes is_lub_unique: "⋀T1 T2 T3 T4. ⟦ ⊢ lub(T1, T2) = T3; ⊢ lub(T1, T2) = T4 ⟧ ⟹ T3 = T4"
shows WT_unique: "⟦ is_lub,P,E ⊢ e :: T; is_lub,P,E ⊢ e :: T' ⟧ ⟹ T = T'"
and WTs_unique: "⟦ is_lub,P,E ⊢ es [::] Ts; is_lub,P,E ⊢ es [::] Ts' ⟧ ⟹ Ts = Ts'"
apply(induct arbitrary: T' and Ts' rule: WT_WTs.inducts)
apply blast
apply blast
apply blast
apply blast
apply fastforce
apply fastforce
apply(fastforce dest: WT_binop_fun)
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply(fastforce dest: sees_field_fun)
apply(fastforce dest: sees_field_fun)
apply blast
apply(fastforce dest: sees_method_fun)
apply fastforce
apply fastforce
apply fastforce
apply(blast dest: is_lub_unique)
apply fastforce
apply fastforce
apply blast
apply fastforce
apply fastforce
done

lemma fixes is_lub
shows wt_env_mono: "is_lub,P,E ⊢ e :: T ⟹ (⋀E'. E ⊆⇩m E' ⟹ is_lub,P,E' ⊢ e :: T)"
and wts_env_mono: "is_lub,P,E ⊢ es [::] Ts ⟹ (⋀E'. E ⊆⇩m E' ⟹ is_lub,P,E' ⊢ es [::] Ts)"
apply(induct rule: WT_WTs.inducts)
apply(fastforce simp: WTCast)
apply(fastforce simp: WTInstanceOf)
apply(fastforce simp: WTVal)
apply(fastforce simp: WTBinOp)
apply(force simp:map_le_def)
apply(fastforce simp: WTFAcc)
apply(fastforce simp: WTFAss del:WT_WTs.intros WT_elim_cases)
apply blast
apply(fastforce)
apply(fastforce simp: map_le_def WTBlock)
apply(fastforce simp: WTSynchronized)
apply(fastforce simp: WTSeq)
apply(fastforce simp: WTCond)
apply(fastforce simp: WTWhile)
apply(fastforce simp: WTThrow)
apply(fastforce simp: WTTry map_le_def dom_def)
apply(fastforce)+
done

lemma fixes is_lub
shows WT_fv: "is_lub,P,E ⊢ e :: T ⟹ fv e ⊆ dom E"
and WT_fvs: "is_lub,P,E ⊢ es [::] Ts ⟹ fvs es ⊆ dom E"
apply(induct rule:WT_WTs.inducts)
apply(simp_all del: fun_upd_apply)
apply fast+
done

lemma fixes is_lub
shows WT_expr_locks: "is_lub,P,E ⊢ e :: T ⟹ expr_locks e = (λad. 0)"
and WTs_expr_lockss: "is_lub,P,E ⊢ es [::] Ts ⟹ expr_lockss es = (λad. 0)"
by(induct rule: WT_WTs.inducts)(auto)

lemma
fixes is_lub :: "ty ⇒ ty ⇒ ty ⇒ bool" ("⊢ lub'((_,/ _)') = _" [51,51,51] 50)
assumes is_lub_is_type: "⋀T1 T2 T3. ⟦ ⊢ lub(T1, T2) = T3; is_type P T1; is_type P T2 ⟧ ⟹ is_type P T3"
and wf: "wf_prog wf_md P"
shows WT_is_type: "⟦ is_lub,P,E ⊢ e :: T; ran E ⊆ types P ⟧ ⟹ is_type P T"
and WTs_is_type: "⟦ is_lub,P,E ⊢ es [::] Ts; ran E ⊆ types P ⟧ ⟹ set Ts ⊆ types P"
apply(induct rule: WT_WTs.inducts)
apply simp
apply simp
apply simp
apply simp
apply (fastforce intro:nth_mem simp add: ran_def)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply simp
apply(fastforce dest: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
apply(fastforce simp add: ran_def split: if_split_asm)
apply(simp)
apply(simp)
apply(fastforce intro: is_lub_is_type)
apply(simp)
apply(simp)
apply simp
apply simp
apply simp
done

lemma
fixes is_lub1 :: "ty ⇒ ty ⇒ ty ⇒ bool" ("⊢1 lub'((_,/ _)') = _" [51,51,51] 50)
and is_lub2 :: "ty ⇒ ty ⇒ ty ⇒ bool" ("⊢2 lub'((_,/ _)') = _" [51,51,51] 50)
assumes wf: "wf_prog wf_md P"
and is_lub1_into_is_lub2: "⋀T1 T2 T3. ⟦ ⊢1 lub(T1, T2) = T3; is_type P T1; is_type P T2 ⟧ ⟹ ⊢2 lub(T1, T2) = T3"
and is_lub2_is_type: "⋀T1 T2 T3. ⟦ ⊢2 lub(T1, T2) = T3; is_type P T1; is_type P T2 ⟧ ⟹ is_type P T3"
shows WT_change_is_lub: "⟦ is_lub1,P,E ⊢ e :: T; ran E ⊆ types P ⟧ ⟹ is_lub2,P,E ⊢ e :: T"
and WTs_change_is_lub: "⟦ is_lub1,P,E ⊢ es [::] Ts; ran E ⊆ types P ⟧ ⟹ is_lub2,P,E ⊢ es [::] Ts"
proof(induct rule: WT_WTs.inducts)
case (WTBlock U E V e' T vo)
from ‹is_type P U› ‹ran E ⊆ types P›
have "ran (E(V ↦ U)) ⊆ types P" by(auto simp add: ran_def)
hence "is_lub2,P,E(V ↦ U) ⊢ e' :: T" by(rule WTBlock)
with ‹is_type P U› show ?case
using ‹case vo of None ⇒ True | ⌊v⌋ ⇒ ∃T'. typeof v = ⌊T'⌋ ∧ P ⊢ T' ≤ U› by auto
next
case (WTCond E e e1 T1 e2 T2 T)
from ‹ran E ⊆ types P› have "is_lub2,P,E ⊢ e :: Boolean" "is_lub2,P,E ⊢ e1 :: T1" "is_lub2,P,E ⊢ e2 :: T2"
by(rule WTCond)+
moreover from is_lub2_is_type wf ‹is_lub2,P,E ⊢ e1 :: T1› ‹ran E ⊆ types P›
have "is_type P T1" by(rule WT_is_type)
from is_lub2_is_type wf ‹is_lub2,P,E ⊢ e2 :: T2› ‹ran E ⊆ types P›
have "is_type P T2" by(rule WT_is_type)
with ‹⊢1 lub(T1, T2) = T› ‹is_type P T1›
have "⊢2 lub(T1, T2) = T" by(rule is_lub1_into_is_lub2)
ultimately show ?case ..
next
case (WTTry E e1 T V C e2)
from ‹ran E ⊆ types P› have "is_lub2,P,E ⊢ e1 :: T" by(rule WTTry)
moreover from ‹P ⊢ C ≼⇧* Throwable› have "is_class P C"
by(rule is_class_sub_Throwable[OF wf])
with ‹ran E ⊆ types P› have "ran (E(V ↦ Class C)) ⊆ types P"
hence "is_lub2,P,E(V ↦ Class C) ⊢ e2 :: T" by(rule WTTry)
ultimately show ?case using ‹P ⊢ C ≼⇧* Throwable› ..
qed auto

subsection ‹Code generator setup›

lemma WTBlock_code:
"⋀is_lub. ⟦ is_type P T; is_lub,P,E(V ↦ T) ⊢ e :: T';
case vo of None ⇒ True | ⌊v⌋ ⇒ case typeof v of None ⇒ False | Some T' ⇒ P ⊢ T' ≤ T ⟧
⟹  is_lub,P,E ⊢ {V:T=vo; e} :: T'"
by(auto)

lemmas [code_pred_intro] =
WTNew WTNewArray WTCast WTInstanceOf WTVal WTVar WTBinOp WTLAss WTAAcc WTAAss WTALength WTFAcc WTFAss WTCAS WTCall
declare
WTBlock_code [code_pred_intro WTBlock']
lemmas [code_pred_intro] =
WTSynchronized WTSeq WTCond WTWhile WTThrow WTTry
WTNil WTCons

code_pred
(modes:
(i ⇒ i ⇒ o ⇒ bool) ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool,
(i ⇒ i ⇒ o ⇒ bool) ⇒ i ⇒ i ⇒ i ⇒ i ⇒ bool)
[detect_switches, skip_proof]
WT
proof -
case WT
from WT.prems show thesis
proof cases
case (WTBlock T V e vo)
thus thesis using WT.WTBlock'[OF refl refl refl, of V T vo e] by(auto)
qed(assumption|erule WT.that[OF refl refl refl]|rule refl)+
next
case WTs
from WTs.prems WTs.that show thesis by cases blast+
qed

inductive is_lub_sup :: "'m prog ⇒ ty ⇒ ty ⇒ ty ⇒ bool"
for P T1 T2 T3
where
"sup P T1 T2 = OK T3 ⟹ is_lub_sup P T1 T2 T3"

code_pred
(modes: i ⇒ i ⇒ i ⇒ o ⇒ bool, i ⇒ i ⇒ i ⇒ i ⇒ bool)
is_lub_sup
.

definition WT_code :: "'addr J_prog ⇒ env ⇒ 'addr expr ⇒ ty ⇒ bool" ("_,_ ⊢ _ ::'' _" [51,51,51] 50)
where "WT_code P ≡ WT (is_lub_sup P) P"

definition WTs_code :: "'addr J_prog ⇒ env ⇒ 'addr expr list ⇒ ty list ⇒ bool" ("_,_ ⊢ _ [::''] _" [51,51,51] 50)
where "WTs_code P ≡ WTs (is_lub_sup P) P"

lemma assumes wf: "wf_prog wf_md P"
shows WT_code_into_WT:
"⟦ P,E ⊢ e ::' T; ran E ⊆ types P ⟧ ⟹ P,E ⊢ e :: T"

and WTs_code_into_WTs:
"⟦ P,E ⊢ es [::'] Ts; ran E ⊆ types P ⟧ ⟹ P,E ⊢ es [::] Ts"
proof -
assume ran: "ran E ⊆ types P"
{ assume wt: "P,E ⊢ e ::' T"
show "P,E ⊢ e :: T"
by(rule WT_change_is_lub[OF wf _ _ wt[unfolded WT_code_def] ran])(blast elim!: is_lub_sup.cases intro: sup_is_lubI[OF wf] is_lub_is_type[OF wf])+ }
{ assume wts: "P,E ⊢ es [::'] Ts"
show "P,E ⊢ es [::] Ts"
by(rule WTs_change_is_lub[OF wf _ _ wts[unfolded WTs_code_def] ran])(blast elim!: is_lub_sup.cases intro: sup_is_lubI[OF wf] is_lub_is_type[OF wf])+ }
qed

lemma assumes wf: "wf_prog wf_md P"
shows WT_into_WT_code:
"⟦ P,E ⊢ e :: T; ran E ⊆ types P ⟧ ⟹ P,E ⊢ e ::' T"

and WT_into_WTs_code_OK:
"⟦ P,E ⊢ es [::] Ts; ran E ⊆ types P ⟧ ⟹ P,E ⊢ es [::'] Ts"
proof -
assume ran: "ran E ⊆ types P"
{ assume wt: "P,E ⊢ e :: T"
show "P,E ⊢ e ::' T" unfolding WT_code_def
by(rule WT_change_is_lub[OF wf _ _ wt ran])(blast intro!: is_lub_sup.intros intro: is_lub_subD[OF wf] sup_is_type[OF wf] elim!: is_lub_sup.cases)+ }
{ assume wts: "P,E ⊢ es [::] Ts"
show "P,E ⊢ es [::'] Ts" unfolding WTs_code_def
by(rule WTs_change_is_lub[OF wf _ _ wts ran])(blast intro!: is_lub_sup.intros intro: is_lub_subD[OF wf] sup_is_type[OF wf] elim!: is_lub_sup.cases)+ }
qed

theorem WT_eq_WT_code:
assumes "wf_prog wf_md P"
and "ran E ⊆ types P"
shows "P,E ⊢ e :: T ⟷ P,E ⊢ e ::' T"
using assms by(blast intro: WT_code_into_WT WT_into_WT_code)

code_pred
(modes: i ⇒ i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ bool)
[inductify]
WT_code
.

code_pred
(modes: i ⇒ i ⇒ i ⇒ i ⇒ bool, i ⇒ i ⇒ i ⇒ o ⇒ bool)
[inductify]
WTs_code
.

end
```