Theory J1WellForm

(*  Title:      JinjaThreads/Compiler/WellType1.thy
    Author:     Andreas Lochbihler, Tobias Nipkow
*)

header {* \isaheader{Well-Formedness of Intermediate Language} *}

theory J1WellForm
imports "../J/JWellForm" J1
begin

subsection "Well-Typedness"

types 
  env1  = "ty list"   --"type environment indexed by variable number"

inductive WT1 :: "J1_prog => env1 => expr1 => ty => bool" ("_,_ \<turnstile>1 _ :: _"   [51,0,0,51] 50)
  and WTs1 :: "J1_prog => env1 => expr1 list => ty list => bool" ("_,_ \<turnstile>1 _ [::] _"   [51,0,0,51]50)
  for P :: J1_prog
  where

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

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

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

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

| WT1Var:
  "[| E!V = T; V < size E |] ==>
  P,E \<turnstile>1 Var V :: T"

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

| WT1LAss:
  "[| E!i = T;  i < size E; P,E \<turnstile>1 e :: T';  P \<turnstile> T' ≤ T |]
  ==> P,E \<turnstile>1 i:=e :: Void"

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

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

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

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

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

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

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

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

| WT1Synchronized:
  "[| P,E \<turnstile>1 o' :: T; is_refT T; T ≠ NT; P,E@[Class Object] \<turnstile>1 e :: T' |]
  ==> P,E \<turnstile>1 syncV (o') e :: T'"

| WT1Seq:
  "[| P,E \<turnstile>1 e1::T1;  P,E \<turnstile>1 e2::T2 |]
  ==>  P,E \<turnstile>1 e1;;e2 :: T2"

| WT1Cond:
  "[| P,E \<turnstile>1 e :: Boolean;  P,E \<turnstile>1 e1::T1;  P,E \<turnstile>1 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>1 if (e) e1 else e2 :: T"

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

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

| WT1Try:
  "[| P,E \<turnstile>1 e1 :: T;  P,E@[Class C] \<turnstile>1 e2 :: T; is_class P C |]
  ==> P,E \<turnstile>1 try e1 catch(C V) e2 :: T"

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

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

declare WT1_WTs1.intros[intro!]
declare WT1Nil[iff]
declare WT1Call[rule del, intro]
declare WT1External[rule del, intro]

inductive_cases WT1_WTs1_cases[elim!]:
  "P,E \<turnstile>1 Val v :: T"
  "P,E \<turnstile>1 Var i :: T"
  "P,E \<turnstile>1 Cast D e :: T"
  "P,E \<turnstile>1 i:=e :: T"
  "P,E \<turnstile>1 {i:U=vo; e} :: T"
  "P,E \<turnstile>1 e1;;e2 :: T"
  "P,E \<turnstile>1 if (e) e1 else e2 :: T"
  "P,E \<turnstile>1 while (e) c :: T"
  "P,E \<turnstile>1 throw e :: T"
  "P,E \<turnstile>1 try e1 catch(C i) e2 :: T"
  "P,E \<turnstile>1 e•F{D} :: T"
  "P,E \<turnstile>1 e1•F{D}:=e2 :: T"
  "P,E \<turnstile>1 e1 «bop» e2 :: T"
  "P,E \<turnstile>1 new C :: T"
  "P,E \<turnstile>1 newA T'⌊e⌉ :: T"
  "P,E \<turnstile>1 a⌊i⌉ := e :: T"
  "P,E \<turnstile>1 a⌊i⌉ :: T"
  "P,E \<turnstile>1 a•length :: T"
  "P,E \<turnstile>1 e•M(es) :: T"
  "P,E \<turnstile>1 syncV (o') e :: T"
  "P,E \<turnstile>1 insyncV (a) e :: T"
  "P,E \<turnstile>1 [] [::] Ts"
  "P,E \<turnstile>1 e#es [::] Ts"

lemma WTs1_same_size: "P,E \<turnstile>1 es [::] Ts ==> size es = size Ts"
by (induct es arbitrary: Ts) auto

lemma WTs1_snoc_cases:
  assumes wt: "P,E \<turnstile>1 es @ [e] [::] Ts"
  obtains T Ts' where "P,E \<turnstile>1 es [::] Ts'" "P,E \<turnstile>1 e :: T"
proof -
  from wt have "∃T Ts'. P,E \<turnstile>1 es [::] Ts' ∧ P,E \<turnstile>1 e :: T"
    by(induct es arbitrary: Ts) auto
  thus thesis by(auto intro: that)
qed

lemma WTs1_append:
  assumes wt: "P,Env \<turnstile>1 es @ es' [::] Ts"
  obtains Ts' Ts'' where "P,Env \<turnstile>1 es [::] Ts'" "P,Env \<turnstile>1 es' [::] Ts''"
proof -
  from wt have "∃Ts' Ts''. P,Env \<turnstile>1 es [::] Ts' ∧ P,Env \<turnstile>1 es' [::] Ts''"
    by(induct es arbitrary: Ts) auto
  thus ?thesis by(auto intro: that)
qed

lemma WT1_not_contains_insync: "P,E \<turnstile>1 e :: T ==> ¬ contains_insync e"
  and WTs1_not_contains_insyncs: "P,E \<turnstile>1 es [::] Ts ==> ¬ contains_insyncs es"
by(induct rule: WT1_WTs1.inducts) auto

lemma WT1_expr_locks: "P,E \<turnstile>1 e :: T ==> expr_locks e = (λa. 0)"
  and WTs1_expr_lockss: "P,E \<turnstile>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 \<turnstile>1 e :: T1 ==> P,E \<turnstile>1 e :: T2 ==> T1 = T2" 
  and WTs1_unique: "P,E \<turnstile>1 es [::] Ts1 ==> P,E \<turnstile>1 es [::] Ts2 ==> Ts1 = Ts2"
apply(induct arbitrary: T2 and Ts2 rule:WT1_WTs1.inducts)
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

apply(erule WT1_WTs1_cases)
 apply (blast dest:sees_method_idemp sees_method_fun)
apply(fastsimp dest: external_WT_is_external_call list_all2_lengthD WTs1_same_size)

apply(fastsimp dest: external_WT_is_external_call list_all2_lengthD WTs1_same_size external_WT_determ)
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
apply blast
done

lemma assumes wf: "wf_prog p P"
  shows WT1_is_type: "P,E \<turnstile>1 e :: T ==> set E ⊆ is_type P ==> is_type P T"
  and "P,E \<turnstile>1 es [::] Ts ==> set E ⊆ is_type P ==> set Ts ⊆ is_type P"
apply(induct rule:WT1_WTs1.inducts)
apply simp
apply simp
apply simp
apply (simp add:typeof_lit_is_type)
apply (fastsimp intro:nth_mem simp add: mem_def)
apply(simp add: WT_binop_is_type)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply (simp add:sees_field_is_type[OF _ wf])
apply simp
apply(fastsimp dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
apply(fastsimp dest: WT_external_is_type)
apply(simp add: mem_def)
apply(simp add: is_class_Object[OF wf] mem_def)
apply simp
apply blast
apply simp
apply simp
apply simp
apply simp
apply(simp add: mem_def)
done

lemma blocks1_WT:
  "[| P,Env @ Ts \<turnstile>1 body :: T; set Ts ⊆ is_type P |] ==> P,Env \<turnstile>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 n T' Ts e)
  note IH = `!!Env. [|P,Env @ Ts \<turnstile>1 e :: T; set Ts ⊆ is_type P; Suc n = length Env|]
              ==> P,Env \<turnstile>1 blocks1 (length Env) Ts e :: T`
  from `set (T' # Ts) ⊆ is_type P` have "set Ts ⊆ is_type P" "is_type P T'" by(auto simp add: mem_def)
  moreover from `P,Env @ T' # Ts \<turnstile>1 e :: T` have "P,(Env @ [T']) @ Ts \<turnstile>1 e :: T" by simp
  note IH[OF this] `n = length Env`
  ultimately show ?case by auto
qed

subsection{* Well-formedness*}

--"Indices in blocks increase by 1"

consts
  \<B> :: "expr1 => nat => bool"
  \<B>s :: "expr1 list => nat => bool"
primrec
"\<B> (new C) i = True"
"\<B> (newA T⌊e⌉) i = \<B> e i"
"\<B> (Cast C e) i = \<B> e i"
"\<B> (Val v) i = True"
"\<B> (e1 «bop» e2) i = (\<B> e1 i ∧ \<B> e2 i)"
"\<B> (Var j) i = True"
"\<B> (j:=e) i = \<B> e i"
"\<B> (a⌊j⌉) i = (\<B> a i ∧ \<B> j i)"
"\<B> (a⌊j⌉:=e) i = (\<B> a i ∧ \<B> j i ∧ \<B> e i)"
"\<B> (a•length) i = \<B> a i"
"\<B> (e•F{D}) i = \<B> e i"
"\<B> (e1•F{D} := e2) i = (\<B> e1 i ∧ \<B> e2 i)"
"\<B> (e•M(es)) i = (\<B> e i ∧ \<B>s es i)"
"\<B> ({j:T=vo; e}) i = (i = j ∧ \<B> e (i+1))"
"\<B> (syncV (o') e) i = (i = V ∧ \<B> o' i ∧ \<B> e (i+1))"
"\<B> (insyncV (a) e) i = (i = V ∧ \<B> e (i+1))"
"\<B> (e1;;e2) i = (\<B> e1 i ∧ \<B> e2 i)"
"\<B> (if (e) e1 else e2) i = (\<B> e i ∧ \<B> e1 i ∧ \<B> e2 i)"
"\<B> (throw e) i = \<B> e i"
"\<B> (while (e) c) i = (\<B> e i ∧ \<B> c i)"
"\<B> (try e1 catch(C j) e2) i = (\<B> e1 i ∧ i=j ∧ \<B> e2 (i+1))"

"\<B>s [] i = True"
"\<B>s (e#es) i = (\<B> e i ∧ \<B>s es i)"

lemma Bs_append [simp]: "\<B>s (es @ es') n <-> \<B>s es n ∧ \<B>s es' n"
by(induct es) auto

lemma Bs_map_Val [simp]: "\<B>s (map Val vs) n"
by(induct vs) auto

lemma B_blocks1 [intro]: "\<B> body (n + length Ts) ==> \<B> (blocks1 n Ts body) n"
by(induct n Ts body rule: blocks1.induct)(auto)

lemma B_extRet2J [simp]: "\<B> (extRet2J va) n"
by(cases va) auto

lemma B_inline_call: "[| \<B> e n; !!n. \<B> e' n |] ==> \<B> (inline_call e' e) n"
  and Bs_inline_calls: "[| \<B>s es n; !!n. \<B> e' n |] ==> \<B>s (inline_calls e' es) n"
by(induct e and es arbitrary: n and n) auto

lemma red1_preserves_B: "[| P \<turnstile>1 ⟨e, s⟩ -ta-> ⟨e', s'⟩; \<B> e n|] ==> \<B> e' n"
  and reds1_preserves_Bs: "[| P \<turnstile>1 ⟨es, s⟩ [-ta->] ⟨es', s'⟩; \<B>s es n|] ==> \<B>s es' n"
by(induct arbitrary: n and n rule: red1_reds1.inducts)(auto)


primrec syncvars :: "('a, 'a) exp => bool"
  and syncvarss :: "('a, 'a) exp list => bool"
where
  "syncvars (new C) = True"
| "syncvars (newA T⌊e⌉) = syncvars e"
| "syncvars (Cast T e) = syncvars e"
| "syncvars (Val v) = True"
| "syncvars (e1 «bop» e2) = (syncvars e1 ∧ syncvars e2)"
| "syncvars (Var V) = True"
| "syncvars (V:=e) = syncvars e"
| "syncvars (a⌊i⌉) = (syncvars a ∧ syncvars i)"
| "syncvars (a⌊i⌉ := e) = (syncvars a ∧ syncvars i ∧ syncvars e)"
| "syncvars (a•length) = syncvars a"
| "syncvars (e•F{D}) = syncvars e"
| "syncvars (e•F{D} := e2) = (syncvars e ∧ syncvars e2)"
| "syncvars (e•M(es)) = (syncvars e ∧ syncvarss es)"
| "syncvars {V:T=vo;e} = syncvars e"
| "syncvars (syncV (e1) e2) = (syncvars e1 ∧ syncvars e2 ∧ V ∉ fv e2)"
| "syncvars (insyncV (a) e) = (syncvars e ∧ V ∉ fv e)"
| "syncvars (e1;;e2) = (syncvars e1 ∧ syncvars e2)"
| "syncvars (if (b) e1 else e2) = (syncvars b ∧ syncvars e1 ∧ syncvars e2)"
| "syncvars (while (b) c) = (syncvars b ∧ syncvars c)"
| "syncvars (throw e) = syncvars e"
| "syncvars (try e1 catch(C V) e2) = (syncvars e1 ∧ syncvars e2)"

| "syncvarss [] = True"
| "syncvarss (e#es) = (syncvars e ∧ syncvarss es)"

lemma syncvarss_append [simp]: "syncvarss (es @ es') <-> syncvarss es ∧ syncvarss es'"
by(induct es) auto

lemma syncvarss_map_Val [simp]: "syncvarss (map Val vs)"
by(induct vs) auto

definition bsok :: "expr1 => nat => bool"
where "bsok e n ≡ \<B> e n ∧ expr_locks e = (λad. 0)"

definition bsoks :: "expr1 list => nat => bool"
where "bsoks es n ≡ \<B>s es n ∧ expr_lockss es = (λad. 0)"

lemma bsok_simps [simp]:
  "bsok (new C) n = True"
  "bsok (newA T⌊e⌉) n = bsok e n"
  "bsok (Cast T e) n = bsok e n"
  "bsok (e1 «bop» e2) n = (bsok e1 n ∧ bsok e2 n)"
  "bsok (Var V) n = True"
  "bsok (Val v) n = True"
  "bsok (V := e) n = bsok e n"
  "bsok (a⌊i⌉) n = (bsok a n ∧ bsok i n)"
  "bsok (a⌊i⌉ := e) n = (bsok a n ∧ bsok i n ∧ bsok e n)"
  "bsok (a•length) n = bsok a n"
  "bsok (e•F{D}) n = bsok e n"
  "bsok (e•F{D} := e') n = (bsok e n ∧ bsok e' n)"
  "bsok (e•M(ps)) n = (bsok e n ∧ bsoks ps n)"
  "bsok {V:T=vo; e} n = (bsok e (Suc n) ∧ V = n)"
  "bsok (syncV (e) e') n = (bsok e n ∧ bsok e' (Suc n) ∧ V = n)"
  "bsok (insyncV (ad) e) n = False"
  "bsok (e;; e') n = (bsok e n ∧ bsok e' n)"
  "bsok (if (e) e1 else e2) n = (bsok e n ∧ bsok e1 n ∧ bsok e2 n)"
  "bsok (while (b) c) n = (bsok b n ∧ bsok c n)"
  "bsok (throw e) n = bsok e n"
  "bsok (try e catch(C V) e') n = (bsok e n ∧ bsok e' (Suc n) ∧ V = n)"
  and bsoks_simps [simp]:
  "bsoks [] n = True"
  "bsoks (e # es) n = (bsok e n ∧ bsoks es n)"
by(auto simp add: bsok_def bsoks_def expand_fun_eq)

lemma WT1_fv: "[| P,E \<turnstile>1 e :: T; \<B> e (length E); syncvars e |] ==> fv e ⊆ {0..<length E}"
  and WTs1_fvs: "[| P,E \<turnstile>1 es [::] Ts; \<B>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 = `[|\<B> e1 (length E); syncvars e1|] ==> fv e1 ⊆ {0..<length E}`
  note IH2 = `[|\<B> e2 (length (E @ [Class Object])); syncvars e2|] ==> fv e2 ⊆ {0..<length (E @ [Class Object])}`
  from `\<B> (syncV (e1) e2) (length E)` have [simp]: "V = length E"
    and B1: "\<B> e1 (length E)" and B2: "\<B> e2 (Suc (length E))" by auto
  from `syncvars (syncV (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 fastsimp+


definition wf_J1_mdecl :: "J1_prog => cname => expr1 mdecl => bool"
where
  "wf_J1_mdecl P C  ≡  λ(M,Ts,T,body).
    (∃T'. P,Class C#Ts \<turnstile>1 body :: T' ∧ P \<turnstile> T' ≤ T) ∧
    \<D> body ⌊{..size Ts}⌋ ∧ \<B> body (size Ts + 1) ∧ syncvars body"

lemma wf_J1_mdecl[simp]:
  "wf_J1_mdecl P C (M,Ts,T,body) ≡
    ((∃T'. P,Class C#Ts \<turnstile>1 body :: T' ∧ P \<turnstile> T' ≤ T) ∧
     \<D> body ⌊{..size Ts}⌋ ∧ \<B> body (size Ts + 1)) ∧ syncvars body"
by (simp add:wf_J1_mdecl_def)

abbreviation wf_J1_prog :: "J1_prog => bool"
where "wf_J1_prog == wf_prog wf_J1_mdecl"

end