Theory J1WellForm

(*  Title:      Jinja/Compiler/WellType1.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Well-Formedness of Intermediate Language›

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

subsection "Well-Typedness"

type_synonym 
  env1  = "ty list"   ― ‹type environment indexed by variable number›

inductive
  WT1 :: "[J1_prog,env1, expr1     , ty     ] ⇒ bool"
         ("(_,_ ⊢1/ _ :: _)"   [51,51,51]50)
  and WTs1 :: "[J1_prog,env1, expr1 list, ty list] ⇒ bool"
         ("(_,_ ⊢1/ _ [::] _)" [51,51,51]50)
  for P :: J1_prog
where
  
  WTNew1:
  "is_class P C  ⟹
  P,E ⊢1 new C :: Class C"

| WTCast1:
  "⟦ P,E ⊢1 e :: Class D;  is_class P C;  P ⊢ C ≼* D ∨ P ⊢ D ≼* C ⟧
  ⟹ P,E ⊢1 Cast C e :: Class C"

| WTVal1:
  "typeof v = Some T ⟹
  P,E ⊢1 Val v :: T"

| WTVar1:
  "⟦ E!i = T; i < size E ⟧
  ⟹ P,E ⊢1 Var i :: T"

| WTBinOp1:
  "⟦ P,E ⊢1 e1 :: T1;  P,E ⊢1 e2 :: T2;
     case bop of Eq ⇒ (P ⊢ T1 ≤ T2 ∨ P ⊢ T2 ≤ T1) ∧ T = Boolean
               | Add ⇒ T1 = Integer ∧ T2 = Integer ∧ T = Integer ⟧
  ⟹ P,E ⊢1 e1 «bop» e2 :: T"

| WTLAss1:
  "⟦ E!i = T;  i < size E; P,E ⊢1 e :: T';  P ⊢ T' ≤ T ⟧
  ⟹ P,E ⊢1 i:=e :: Void"

| WTFAcc1:
  "⟦ P,E ⊢1 e :: Class C;  P ⊢ C sees F:T in D ⟧
  ⟹ P,E ⊢1 e∙F{D} :: T"

| WTFAss1:
  "⟦ P,E ⊢1 e1 :: Class C;  P ⊢ C sees F:T in D;  P,E ⊢1 e2 :: T';  P ⊢ T' ≤ T ⟧
  ⟹ P,E ⊢1 e1∙F{D} := e2 :: Void"

| WTCall1:
  "⟦ P,E ⊢1 e :: Class 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"

| WTBlock1:
  "⟦ is_type P T; P,E@[T] ⊢1 e::T' ⟧
  ⟹  P,E ⊢1 {i:T; e} :: T'"

| WTSeq1:
  "⟦ P,E ⊢1 e1::T1;  P,E ⊢1 e2::T2 ⟧
  ⟹  P,E ⊢1 e1;;e2 :: T2"

| WTCond1:
  "⟦ P,E ⊢1 e :: Boolean;  P,E ⊢1 e1::T1;  P,E ⊢1 e2::T2;
    P ⊢ T1 ≤ T2 ∨ P ⊢ T2 ≤ T1;  P ⊢ T1 ≤ T2 ⟶ T = T2; P ⊢ T2 ≤ T1 ⟶ T = T1 ⟧
  ⟹ P,E ⊢1 if (e) e1 else e2 :: T"

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

| WTThrow1:
  "P,E ⊢1 e :: Class C  ⟹
  P,E ⊢1 throw e :: Void"

| WTTry1:
  "⟦ P,E ⊢1 e1 :: T;  P,E@[Class C] ⊢1 e2 :: T; is_class P C ⟧
  ⟹ P,E ⊢1 try e1 catch(C i) e2 :: T"

| WTNil1:
  "P,E ⊢1 [] [::] []"

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

(*<*)
declare  WT1_WTs1.intros[intro!]
declare WTNil1[iff]

lemmas WT1_WTs1_induct = WT1_WTs1.induct [split_format (complete)]
  and WT1_WTs1_inducts = WT1_WTs1.inducts [split_format (complete)]

inductive_cases eee[elim!]:
  "P,E ⊢1 Val v :: T"
  "P,E ⊢1 Var i :: T"
  "P,E ⊢1 Cast D e :: T"
  "P,E ⊢1 i:=e :: T"
  "P,E ⊢1 {i:U; 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 e1 «bop» e2 :: T"
  "P,E ⊢1 new C :: T"
  "P,E ⊢1 e∙M(es) :: T"
  "P,E ⊢1 [] [::] Ts"
  "P,E ⊢1 e#es [::] Ts"
(*>*)

lemma WTs1_same_size: "⋀Ts. P,E ⊢1 es [::] Ts ⟹ size es = size Ts"
(*<*)by (induct es type:list) auto(*>*)


lemma WT1_unique:
  "P,E ⊢1 e :: T1 ⟹ (⋀T2. P,E ⊢1 e :: T2 ⟹ T1 = T2)" and
  "P,E ⊢1 es [::] Ts1 ⟹ (⋀Ts2. P,E ⊢1 es [::] Ts2 ⟹ Ts1 = Ts2)"
(*<*)
proof(induct rule:WT1_WTs1.inducts)
  case WTVal1 then show ?case by clarsimp
next
  case (WTBinOp1 E e1 T1 e2 T2 bop T)
  then show ?case by(case_tac bop) force+
next
  case WTFAcc1 then show ?case
    by (blast dest:sees_field_idemp sees_field_fun)
next
  case WTCall1 then show ?case
    by (blast dest:sees_method_idemp sees_method_fun)
qed blast+
(*>*)


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 "P,E ⊢1 es [::] Ts ⟹ True"
(*<*)
proof(induct rule:WT1_WTs1.inducts)
  case WTVal1 then show ?case by (simp add:typeof_lit_is_type)
next
  case WTVar1 then show ?case by (blast intro:nth_mem)
next
  case WTBinOp1 then show ?case by (simp split:bop.splits)
next
  case WTFAcc1 then show ?case
    by (simp add:sees_field_is_type[OF _ wf])
next
  case WTCall1 then show ?case
    by (fastforce dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
next
  case WTCond1 then show ?case by blast
qed simp+
(*>*)


subsection‹Well-formedness›

― ‹Indices in blocks increase by 1›

primrec ℬ :: "expr1 ⇒ nat ⇒ bool"
  and ℬs :: "expr1 list ⇒ nat ⇒ bool" where
"ℬ (new C) i = True" |
"ℬ (Cast C e) i = ℬ e i" |
"ℬ (Val v) i = True" |
"ℬ (e1 «bop» e2) i = (ℬ e1 i ∧ ℬ e2 i)" |
"ℬ (Var j) i = True" |
"ℬ (e∙F{D}) i = ℬ e i" |
"ℬ (j:=e) i = ℬ e i" |
"ℬ (e1∙F{D} := e2) i = (ℬ e1 i ∧ ℬ e2 i)" |
"ℬ (e∙M(es)) i = (ℬ e i ∧ ℬs es i)" |
"ℬ ({j:T ; e}) i = (i = j ∧ ℬ e (i+1))" |
"ℬ (e1;;e2) i = (ℬ e1 i ∧ ℬ e2 i)" |
"ℬ (if (e) e1 else e2) i = (ℬ e i ∧ ℬ e1 i ∧ ℬ e2 i)" |
"ℬ (throw e) i = ℬ e i" |
"ℬ (while (e) c) i = (ℬ e i ∧ ℬ c i)" |
"ℬ (try e1 catch(C j) e2) i = (ℬ e1 i ∧ i=j ∧ ℬ e2 (i+1))" |

"ℬs [] i = True" |
"ℬs (e#es) i = (ℬ e i ∧ ℬs es i)"


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 ⊢1 body :: T' ∧ P ⊢ T' ≤ T) ∧
    𝒟 body ⌊{..size Ts}⌋ ∧ ℬ body (size Ts + 1)"

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

abbreviation "wf_J1_prog == wf_prog wf_J1_mdecl"

end