Theory J1WellForm

(*  Title:      Jinja/Compiler/WellType1.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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

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

subsection "Well-Typedness"

type_synonym 
  env⇣1  = "ty list"   --"type environment indexed by variable number"

inductive
  WT⇣1 :: "[J⇣1_prog,env⇣1, expr⇣1     , ty     ] => bool"
         ("(_,_ \<turnstile>⇩1/ _ :: _)"   [51,51,51]50)
  and WTs⇣1 :: "[J⇣1_prog,env⇣1, expr⇣1 list, ty list] => bool"
         ("(_,_ \<turnstile>⇩1/ _ [::] _)" [51,51,51]50)
  for P :: J⇣1_prog
where
  
  WTNew⇣1:
  "is_class P C  ==>
  P,E \<turnstile>⇩1 new C :: Class C"

| WTCast⇣1:
  "[| P,E \<turnstile>⇩1 e :: Class D;  is_class P C;  P \<turnstile> C \<preceq>⇧* D ∨ P \<turnstile> D \<preceq>⇧* C |]
  ==> P,E \<turnstile>⇩1 Cast C e :: Class C"

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

| WTVar⇣1:
  "[| E!i = T; i < size E |]
  ==> P,E \<turnstile>⇩1 Var i :: T"

| WTBinOp⇣1:
  "[| P,E \<turnstile>⇩1 e⇣1 :: T⇣1;  P,E \<turnstile>⇩1 e⇣2 :: T⇣2;
     case bop of Eq => (P \<turnstile> T⇣1 ≤ T⇣2 ∨ P \<turnstile> T⇣2 ≤ T⇣1) ∧ T = Boolean
               | Add => T⇣1 = Integer ∧ T⇣2 = Integer ∧ T = Integer |]
  ==> P,E \<turnstile>⇩1 e⇣1 «bop» e⇣2 :: T"

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

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

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

| WTCall⇣1:
  "[| P,E \<turnstile>⇩1 e :: Class C; 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"

| WTBlock⇣1:
  "[| is_type P T; P,E@[T] \<turnstile>⇩1 e::T' |]
  ==>  P,E \<turnstile>⇩1 {i:T; e} :: T'"

| WTSeq⇣1:
  "[| P,E \<turnstile>⇩1 e⇣1::T⇣1;  P,E \<turnstile>⇩1 e⇣2::T⇣2 |]
  ==>  P,E \<turnstile>⇩1 e⇣1;;e⇣2 :: T⇣2"

| WTCond⇣1:
  "[| P,E \<turnstile>⇩1 e :: Boolean;  P,E \<turnstile>⇩1 e⇣1::T⇣1;  P,E \<turnstile>⇩1 e⇣2::T⇣2;
    P \<turnstile> T⇣1 ≤ T⇣2 ∨ P \<turnstile> T⇣2 ≤ T⇣1;  P \<turnstile> T⇣1 ≤ T⇣2 --> T = T⇣2; P \<turnstile> T⇣2 ≤ T⇣1 --> T = T⇣1 |]
  ==> P,E \<turnstile>⇩1 if (e) e⇣1 else e⇣2 :: T"

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

| WTThrow⇣1:
  "P,E \<turnstile>⇩1 e :: Class C  ==>
  P,E \<turnstile>⇩1 throw e :: Void"

| WTTry⇣1:
  "[| P,E \<turnstile>⇩1 e⇣1 :: T;  P,E@[Class C] \<turnstile>⇩1 e⇣2 :: T; is_class P C |]
  ==> P,E \<turnstile>⇩1 try e⇣1 catch(C i) e⇣2 :: T"

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

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

(*<*)
declare  WT⇣1_WTs⇣1.intros[intro!]
declare WTNil⇣1[iff]

lemmas WT⇣1_WTs⇣1_induct = WT⇣1_WTs⇣1.induct [split_format (complete)]
  and WT⇣1_WTs⇣1_inducts = WT⇣1_WTs⇣1.inducts [split_format (complete)]

inductive_cases eee[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; e} :: T"
  "P,E \<turnstile>⇩1 e⇣1;;e⇣2 :: T"
  "P,E \<turnstile>⇩1 if (e) e⇣1 else e⇣2 :: T"
  "P,E \<turnstile>⇩1 while (e) c :: T"
  "P,E \<turnstile>⇩1 throw e :: T"
  "P,E \<turnstile>⇩1 try e⇣1 catch(C i) e⇣2 :: T"
  "P,E \<turnstile>⇩1 e•F{D} :: T"
  "P,E \<turnstile>⇩1 e⇣1•F{D}:=e⇣2 :: T"
  "P,E \<turnstile>⇩1 e⇣1 «bop» e⇣2 :: T"
  "P,E \<turnstile>⇩1 new C :: T"
  "P,E \<turnstile>⇩1 e•M(es) :: T"
  "P,E \<turnstile>⇩1 [] [::] Ts"
  "P,E \<turnstile>⇩1 e#es [::] Ts"
(*>*)

lemma WTs⇣1_same_size: "!!Ts. P,E \<turnstile>⇩1 es [::] Ts ==> size es = size Ts"
(*<*)by (induct es type:list) auto(*>*)


lemma WT⇣1_unique:
  "P,E \<turnstile>⇩1 e :: T⇣1 ==> (!!T⇣2. P,E \<turnstile>⇩1 e :: T⇣2 ==> T⇣1 = T⇣2)" and
  "P,E \<turnstile>⇩1 es [::] Ts⇣1 ==> (!!Ts⇣2. P,E \<turnstile>⇩1 es [::] Ts⇣2 ==> Ts⇣1 = Ts⇣2)"
(*<*)
apply(induct rule:WT⇣1_WTs⇣1.inducts)
apply blast
apply blast
apply clarsimp
apply blast
apply clarsimp
apply(case_tac bop)
apply clarsimp
apply clarsimp
apply blast
apply (blast dest:sees_field_idemp sees_field_fun)
apply blast
apply (blast dest:sees_method_idemp sees_method_fun)
apply blast
apply blast
apply blast
apply blast
apply clarify
apply blast
apply blast
apply blast
done
(*>*)


lemma assumes wf: "wf_prog p P"
shows WT⇣1_is_type: "P,E \<turnstile>⇩1 e :: T ==> set E ⊆ types P ==> is_type P T"
and "P,E \<turnstile>⇩1 es [::] Ts ==> True"
(*<*)
apply(induct rule:WT⇣1_WTs⇣1.inducts)
apply simp
apply simp
apply (simp add:typeof_lit_is_type)
apply (blast intro:nth_mem)
apply(simp split:bop.splits)
apply simp
apply (simp add:sees_field_is_type[OF _ wf])
apply simp
apply(fastforce dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
apply simp
apply simp
apply blast
apply simp
apply simp
apply simp
apply simp
apply simp
done
(*>*)


subsection{* Well-formedness*}

--"Indices in blocks increase by 1"

primrec \<B> :: "expr⇣1 => nat => bool"
  and \<B>s :: "expr⇣1 list => nat => bool" where
"\<B> (new C) i = True" |
"\<B> (Cast C e) i = \<B> e i" |
"\<B> (Val v) i = True" |
"\<B> (e⇣1 «bop» e⇣2) i = (\<B> e⇣1 i ∧ \<B> e⇣2 i)" |
"\<B> (Var j) i = True" |
"\<B> (e•F{D}) i = \<B> e i" |
"\<B> (j:=e) i = \<B> e i" |
"\<B> (e⇣1•F{D} := e⇣2) i = (\<B> e⇣1 i ∧ \<B> e⇣2 i)" |
"\<B> (e•M(es)) i = (\<B> e i ∧ \<B>s es i)" |
"\<B> ({j:T ; e}) i = (i = j ∧ \<B> e (i+1))" |
"\<B> (e⇣1;;e⇣2) i = (\<B> e⇣1 i ∧ \<B> e⇣2 i)" |
"\<B> (if (e) e⇣1 else e⇣2) i = (\<B> e i ∧ \<B> e⇣1 i ∧ \<B> e⇣2 i)" |
"\<B> (throw e) i = \<B> e i" |
"\<B> (while (e) c) i = (\<B> e i ∧ \<B> c i)" |
"\<B> (try e⇣1 catch(C j) e⇣2) i = (\<B> e⇣1 i ∧ i=j ∧ \<B> e⇣2 (i+1))" |

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


definition wf_J⇣1_mdecl :: "J⇣1_prog => cname => expr⇣1 mdecl => bool"
where
  "wf_J⇣1_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)"

lemma wf_J⇣1_mdecl[simp]:
  "wf_J⇣1_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))"
(*<*)by (simp add:wf_J⇣1_mdecl_def)(*>*)

abbreviation "wf_J⇣1_prog == wf_prog wf_J⇣1_mdecl"

end