Theory WellType

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

header {* \isaheader{Well-typedness of Jinja expressions} *}

theory WellType
imports Expr State "../Common/ExternalCall"
begin

types 
  env  = "vname \<rightharpoonup> ty"

inductive WT :: "J_prog => env => expr => ty => bool" ("_,_ \<turnstile> _ :: _"   [51,51,51]50)
  and WTs :: "J_prog => env => expr list => ty list => bool" ("_,_ \<turnstile> _ [::] _"   [51,51,51]50)
  for P :: "J_prog"
  where

  WTNew:
  "is_class P C  ==>
  P,E \<turnstile> new C :: Class C"

| WTNewArray:
  "[| P,E \<turnstile> e :: Integer; is_type P T |] ==>
  P,E \<turnstile> newA T⌊e⌉ :: T⌊⌉"

| WTCast:
  "[| P,E \<turnstile> e :: T; P \<turnstile> U ≤ T ∨ P \<turnstile> T ≤ U; is_type P U |]
  ==> P,E \<turnstile> Cast U e :: U"

| WTVal:
  "typeof v = Some T ==>
  P,E \<turnstile> Val v :: T"

| WTVar:
  "E V = Some T ==>
  P,E \<turnstile> Var V :: T"

| WTBinOp:
  "[| P,E \<turnstile> e1 :: T1; P,E \<turnstile> e2 :: T2; P \<turnstile> T1«bop»T2 :: T |]
  ==> P,E \<turnstile> e1«bop»e2 :: T"

| WTLAss:
  "[| E V = Some T;  P,E \<turnstile> e :: T';  P \<turnstile> T' ≤ T;  V ≠ this |]
  ==> P,E \<turnstile> V:=e :: Void"

| WTAAcc:
  "[| P,E \<turnstile> a :: T⌊⌉; P,E \<turnstile> i :: Integer |]
  ==> P,E \<turnstile> a⌊i⌉ :: T"

| WTAAss:
  "[| P,E \<turnstile> a :: T⌊⌉; P,E \<turnstile> i :: Integer; P,E \<turnstile> e :: T'; P \<turnstile> T' ≤ T |]
  ==> P,E \<turnstile> a⌊i⌉ := e :: Void"

| WTALength:
  "P,E \<turnstile> a :: T⌊⌉ ==> P,E \<turnstile> a•length :: Integer"

| WTFAcc:
  "[| P,E \<turnstile> e :: Class C;  P \<turnstile> C sees F:T in D |]
  ==> P,E \<turnstile> e•F{D} :: T"

| WTFAss:
  "[| P,E \<turnstile> e1 :: Class C;  P \<turnstile> C sees F:T in D;  P,E \<turnstile> e2 :: T';  P \<turnstile> T' ≤ T |]
  ==> P,E \<turnstile> e1•F{D}:=e2 :: Void"

| WTCall:
  "[| P,E \<turnstile> e :: Class C; ¬ is_external_call P (Class C) M; P \<turnstile> C sees M:Ts -> T = (pns,body) in D;
     P,E \<turnstile> es [::] Ts'; P \<turnstile> Ts' [≤] Ts |]
  ==> P,E \<turnstile> e•M(es) :: T"

| WTExternal:
  "[| P,E \<turnstile> e :: T; P,E \<turnstile> es [::] Ts; P \<turnstile> T•M(Ts) :: U |]
  ==> P,E \<turnstile> e•M(es) :: U"

| WTBlock:
  "[| is_type P T;  P,E(V \<mapsto> T) \<turnstile> e :: T'; case vo of None => True | ⌊v⌋ => ∃T'. typeof v = ⌊T'⌋ ∧ P \<turnstile> T' ≤ T |]
  ==>  P,E \<turnstile> {V:T=vo; e} :: T'"

| WTSynchronized:
  "[| P,E \<turnstile> o' :: T; is_refT T; T ≠ NT; P,E \<turnstile> e :: T' |]
  ==> P,E \<turnstile> sync(o') e :: T'"

(* Note that insync is not statically typable. *)

| WTSeq:
  "[| P,E \<turnstile> e1::T1;  P,E \<turnstile> e2::T2 |]
  ==>  P,E \<turnstile> e1;;e2 :: T2"
| WTCond:
  "[| P,E \<turnstile> e :: Boolean;  P,E \<turnstile> e1::T1;  P,E \<turnstile> e2::T2;
     P \<turnstile> T1 ≤ T2 ∨ P \<turnstile> T2 ≤ T1;  P \<turnstile> T1 ≤ T2 --> T = T2;  P \<turnstile> T2 ≤ T1 --> T = T1 |]
  ==> P,E \<turnstile> if (e) e1 else e2 :: T"

| WTWhile:
  "[| P,E \<turnstile> e :: Boolean;  P,E \<turnstile> c::T |]
  ==> P,E \<turnstile> while (e) c :: Void"

| WTThrow:
  "[| P,E \<turnstile> e :: Class C; P \<turnstile> C \<preceq>* Throwable |] ==> 
  P,E \<turnstile> throw e :: Void"

| WTTry:
  "[| P,E \<turnstile> e1 :: T;  P,E(V \<mapsto> Class C) \<turnstile> e2 :: T; P \<turnstile> C \<preceq>* Throwable |]
  ==> P,E \<turnstile> try e1 catch(C V) e2 :: T"

| WTNil: "P,E \<turnstile> [] [::] []"

| WTCons: "[| P,E \<turnstile> e :: T; P,E \<turnstile> es [::] Ts |] ==> P,E \<turnstile> e#es [::] T#Ts"


declare WT_WTs.intros[intro!]

lemma [iff]: "(P,E \<turnstile> [] [::] Ts) = (Ts = [])"
by (auto elim: WTs.cases)


lemma [iff]: "(P,E \<turnstile> e#es [::] T#Ts) = (P,E \<turnstile> e :: T ∧ P,E \<turnstile> es [::] Ts)"
by (auto elim: WTs.cases)

lemma WTs_conv_list_all2: "P,E \<turnstile> es [::] Ts = list_all2 (WT P E) es Ts"
by(induct es arbitrary: Ts)(auto simp add: list_all2_Cons1 elim: WTs.cases)

lemma [iff]: "(P,E \<turnstile> (e#es) [::] Ts) =
  (∃U Us. Ts = U#Us ∧ P,E \<turnstile> e :: U ∧ P,E \<turnstile> es [::] Us)"
by(simp add: WTs_conv_list_all2 list_all2_Cons1)

lemma [iff]: "!!Ts. (P,E \<turnstile> es1 @ es2 [::] Ts) =
  (∃Ts1 Ts2. Ts = Ts1 @ Ts2 ∧ P,E \<turnstile> es1 [::] Ts1 ∧ P,E \<turnstile> es2[::]Ts2)"
by(auto simp add: WTs_conv_list_all2 list_all2_append1 dest: list_all2_lengthD[symmetric])

lemma [iff]: "P,E \<turnstile> Val v :: T = (typeof v = Some T)"
by (auto elim: WT.cases)

lemma [iff]: "P,E \<turnstile> Var V :: T = (E V = Some T)"
by (auto elim: WT.cases)

lemma [iff]: "P,E \<turnstile> e1;;e2 :: T2 = (∃T1. P,E \<turnstile> e1::T1 ∧ P,E \<turnstile> e2::T2)"
by (auto elim: WT.cases)

lemma [iff]: "(P,E \<turnstile> {V:T=vo; e} :: T') <-> is_type P T ∧ P,E(V\<mapsto>T) \<turnstile> e :: T' ∧ (case vo of None => True | Some v => ∃T'. typeof v = ⌊T'⌋ ∧ P \<turnstile> T' ≤ T)"
by (auto elim: WT.cases)

inductive_cases WT_elim_cases[elim!]:
  "P,E \<turnstile> V :=e :: T"
  "P,E \<turnstile> sync(o') e :: T"
  "P,E \<turnstile> if (e) e1 else e2 :: T"
  "P,E \<turnstile> while (e) c :: T"
  "P,E \<turnstile> throw e :: T"
  "P,E \<turnstile> try e1 catch(C V) e2 :: T"
  "P,E \<turnstile> Cast D e :: T"
  "P,E \<turnstile> a•F{D} :: T"
  "P,E \<turnstile> a•F{D} := v :: T"
  "P,E \<turnstile> e1 «bop» e2 :: T"
  "P,E \<turnstile> new C :: T"
  "P,E \<turnstile> newA T⌊e⌉ :: T'"
  "P,E \<turnstile> a⌊i⌉ := e :: T"
  "P,E \<turnstile> a⌊i⌉ :: T"
  "P,E \<turnstile> a•length :: T"
  "P,E \<turnstile> e•M(ps) :: T"
  "P,E \<turnstile> sync(o') e :: T"
  "P,E \<turnstile> insync(a) e :: T"

inductive_cases WT_callE:
  "P,E \<turnstile> e•M(es) :: T"

lemma WT_unique: "[| P,E \<turnstile> e :: T; P,E \<turnstile> e :: T' |] ==> T = T'"
  and WTs_unique: "[| P,E \<turnstile> es [::] Ts; P,E \<turnstile> es [::] Ts' |] ==> Ts = Ts'"
apply(induct arbitrary: T' and Ts' rule: WT_WTs.inducts)
apply blast
apply blast
apply blast
apply fastsimp
apply fastsimp
apply(fastsimp dest: WT_binop_fun)
apply fastsimp
apply fastsimp
apply fastsimp
apply fastsimp
apply(fastsimp dest: sees_field_fun)
apply(fastsimp dest: sees_field_fun)
apply(erule WT_callE)
 apply(fastsimp dest: sees_method_fun)
apply(fastsimp dest: external_WT_is_external_call)
apply(erule WT_callE)
 apply(fastsimp dest: external_WT_is_external_call)
apply(fastsimp dest: external_WT_determ)
apply fastsimp
apply fastsimp
apply fastsimp
apply force
apply fastsimp
apply fastsimp
apply blast
apply fastsimp
apply fastsimp
done

lemma wt_env_mono: "P,E \<turnstile> e :: T ==> (!!E'. E ⊆m E' ==> P,E' \<turnstile> e :: T)"
  and wts_env_mono: "P,E \<turnstile> es [::] Ts ==> (!!E'. E ⊆m E' ==> P,E' \<turnstile> es [::] Ts)"
apply(induct rule: WT_WTs.inducts)
apply(simp add: WTNew)
apply(simp add: WTNewArray)
apply(fastsimp simp: WTCast)
apply(fastsimp simp: WTVal)
apply(simp add: WTVar map_le_def dom_def)
apply(fastsimp simp: WTBinOp)
apply(force simp:map_le_def)
apply(simp add: WTAAcc)
apply(simp add: WTAAss, fastsimp)
apply(simp add: WTALength, fastsimp)
apply(fastsimp simp: WTFAcc)
apply(fastsimp simp: WTFAss del:WT_WTs.intros WT_elim_cases)
apply(clarsimp, rule WTCall, blast+)[1]
apply(fastsimp)
apply(fastsimp simp: map_le_def WTBlock)
apply(fastsimp simp: WTSynchronized)
apply(fastsimp simp: WTSeq)
apply(fastsimp simp: WTCond)
apply(fastsimp simp: WTWhile)
apply(fastsimp simp: WTThrow)
apply(fastsimp simp: WTTry map_le_def dom_def)
apply(fastsimp)+
done


lemma WT_fv: "P,E \<turnstile> e :: T ==> fv e ⊆ dom E"
  and WT_fvs: "P,E \<turnstile> es [::] Ts ==> fvs es ⊆ dom E"
apply(induct rule:WT_WTs.inducts)
apply(simp_all del: fun_upd_apply)
apply fast+
done

lemma WT_expr_locks: "P,E \<turnstile> e :: T ==> expr_locks e = (λad. 0)"
  and WTs_expr_lockss: "P,E \<turnstile> es [::] Ts ==> expr_lockss es = (λad. 0)"
by(induct rule: WT_WTs.inducts)(auto)

end