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)
  and P :: "'addr J_prog"
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(simp add: WTNew)
apply(simp add: WTNewArray)
apply(fastforce simp: WTCast)
apply(fastforce simp: WTInstanceOf)
apply(fastforce simp: WTVal)
apply(simp add: WTVar map_le_def dom_def)
apply(fastforce simp: WTBinOp)
apply(force simp:map_le_def)
apply(simp add: WTAAcc)
apply(simp add: WTAAss, fastforce)
apply(simp add: WTALength, fastforce)
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 (simp add:typeof_lit_is_type)
apply (fastforce intro:nth_mem simp add: ran_def)
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(fastforce simp add: ran_def split: if_split_asm)
apply(simp add: is_class_Object[OF wf])
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"
    by(auto simp add: ran_def)
  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