Theory J1WellForm

Up to index of Isabelle/HOL/Jinja

theory J1WellForm = JWellForm + J1: 
(*  Title:      Jinja/Compiler/WellType1.thy
    ID:         $Id: J1WellForm.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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

theory J1WellForm = JWellForm + J1:

subsection "Well-Typedness"

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

consts
  WT1 :: "J1_prog => (env1 × expr1      × ty     ) set"
  WTs1:: "J1_prog => (env1 × expr1 list × ty list) set"

(*<*)
syntax (xsymbols)
  WT1 :: "[J1_prog,env1, expr1     , ty     ] => bool"
         ("(_,_ \<turnstile>1/ _ :: _)"   [51,51,51]50)
  WTs1:: "[J1_prog,env1, expr1 list, ty list] => bool"
         ("(_,_ \<turnstile>1/ _ [::] _)" [51,51,51]50)
(*>*)

translations
  "P,E \<turnstile>1 e :: T"  ==  "(E,e,T) ∈ WT1 P"
  "P,E \<turnstile>1 es [::] Ts"  ==  "(E,es,Ts) ∈ WTs1 P"

inductive "WT1 P" "WTs1 P"
intros
  
WTNew1:
  "is_class P C  ==>
  P,E \<turnstile>1 new C :: Class C"

WTCast1:
  "[| 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"

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

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

WTBinOp1:
  "[| P,E \<turnstile>1 e1 :: T1;  P,E \<turnstile>1 e2 :: T2;
     case bop of Eq => (P \<turnstile> T1 ≤ T2 ∨ P \<turnstile> T2 ≤ T1) ∧ T = Boolean
               | Add => T1 = Integer ∧ T2 = Integer ∧ T = Integer |]
  ==> P,E \<turnstile>1 e1 «bop» e2 :: T"

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

WTFAcc1:
  "[| P,E \<turnstile>1 e :: Class C;  P \<turnstile> C sees F:T in D |]
  ==> P,E \<turnstile>1 e\<bullet>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\<bullet>F{D} := e2 :: Void"

WTCall1:
  "[| 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\<bullet>M(es) :: T"

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

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

WTCond1:
  "[| 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"

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

WTThrow1:
  "P,E \<turnstile>1 e :: Class C  ==>
  P,E \<turnstile>1 throw e :: Void"

WTTry1:
  "[| 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 i) e2 :: T"

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

WTCons1:
  "[| 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!] WTNil1[iff]

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

inductive_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; 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\<bullet>F{D} :: T"
  "P,E \<turnstile>1 e1\<bullet>F{D}:=e2 :: T"
  "P,E \<turnstile>1 e1 «bop» e2 :: T"
  "P,E \<turnstile>1 new C :: T"
  "P,E \<turnstile>1 e\<bullet>M(es) :: T"
  "P,E \<turnstile>1 [] [::] Ts"
  "P,E \<turnstile>1 e#es [::] Ts"
(*>*)

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


lemma WT1_unique:
  "P,E \<turnstile>1 e :: T1 ==> (!!T2. P,E \<turnstile>1 e :: T2 ==> T1 = T2)" and
  "P,E \<turnstile>1 es [::] Ts1 ==> (!!Ts2. P,E \<turnstile>1 es [::] Ts2 ==> Ts1 = Ts2)"
(*<*)
apply(induct rule:WT1_WTs1.induct)
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 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 ⊆ types P ==> is_type P T"
and "P,E \<turnstile>1 es [::] Ts ==> True"
(*<*)
apply(induct rule:WT1_WTs1.induct)
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(fastsimp 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"

consts
  \<B> :: "expr1 => nat => bool"
  \<B>s :: "expr1 list => nat => bool"
primrec
"\<B> (new C) i = True"
"\<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> (e\<bullet>F{D}) i = \<B> e i"
"\<B> (j:=e) i = \<B> e i"
"\<B> (e1\<bullet>F{D} := e2) i = (\<B> e1 i ∧ \<B> e2 i)"
"\<B> (e\<bullet>M(es)) i = (\<B> e i ∧ \<B>s es i)"
"\<B> ({j:T ; e}) i = (i = j ∧ \<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)"


constdefs
  wf_J1_mdecl :: "J1_prog => cname => expr1 mdecl => bool"
  "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)"

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))"
(*<*)by (simp add:wf_J1_mdecl_def)(*>*)

(*<*)
syntax
  wf_J1_prog :: "J1_prog => bool"
(*>*)

translations
  "wf_J1_prog"  ==  "wf_prog wf_J1_mdecl"

end

Well-Typedness

lemmas WT1_WTs1_induct: 

  [| !!C E. is_class P C ==> P1 E (new C) (Class C);
     !!C D E e.
        [| WT1 P E e (Class D); P1 E e (Class D); is_class P C;
           subcls P C D | subcls P D C |]
        ==> P1 E (Cast C e) (Class C);
     !!E T v. typeof v = ⌊T⌋ ==> P1 E (Val v) T;
     !!E T i. [| E ! i = T; i < length E |] ==> P1 E (Var i) T;
     !!E T T1 T2 bop e1 e2.
        [| WT1 P E e1 T1; P1 E e1 T1; WT1 P E e2 T2; P1 E e2 T2;
           case bop of Eq => (widen P T1 T2 | widen P T2 T1) & T = Boolean
           | Add => T1 = Integer & T2 = Integer & T = Integer |]
        ==> P1 E (e1 «bop» e2) T;
     !!E T T' e i.
        [| E ! i = T; i < length E; WT1 P E e T'; P1 E e T'; widen P T' T |]
        ==> P1 E (i:=e) Void;
     !!C D E F T e.
        [| WT1 P E e (Class C); P1 E e (Class C);
           P \<turnstile> C sees F:T in D |]
        ==> P1 E (e\<bullet>F{D}) T;
     !!C D E F T T' e1 e2.
        [| WT1 P E e1 (Class C); P1 E e1 (Class C);
           P \<turnstile> C sees F:T in D; WT1 P E e2 T'; P1 E e2 T';
           widen P T' T |]
        ==> P1 E (e1\<bullet>F{D} := e2) Void;
     !!C D E M T Ts Ts' e es m.
        [| WT1 P E e (Class C); P1 E e (Class C);
           P \<turnstile> C sees M: Ts'->T = m in D; WTs1 P E es Ts; P2 E es Ts;
           widens P Ts Ts' |]
        ==> P1 E (e\<bullet>M(es)) T;
     !!E T T' e i.
        [| is_type P T; WT1 P (E @ [T]) e T'; P1 (E @ [T]) e T' |]
        ==> P1 E {i:T; e} T';
     !!E T1 T2 e1 e2.
        [| WT1 P E e1 T1; P1 E e1 T1; WT1 P E e2 T2; P1 E e2 T2 |]
        ==> P1 E (e1;; e2) T2;
     !!E T T1 T2 e e1 e2.
        [| WT1 P E e Boolean; P1 E e Boolean; WT1 P E e1 T1; P1 E e1 T1;
           WT1 P E e2 T2; P1 E e2 T2; widen P T1 T2 | widen P T2 T1;
           widen P T1 T2 --> T = T2; widen P T2 T1 --> T = T1 |]
        ==> P1 E (if (e) e1 else e2) T;
     !!E T c e.
        [| WT1 P E e Boolean; P1 E e Boolean; WT1 P E c T; P1 E c T |]
        ==> P1 E (while (e) c) Void;
     !!C E e. [| WT1 P E e (Class C); P1 E e (Class C) |] ==> P1 E (throw e) Void;
     !!C E T e1 e2 i.
        [| WT1 P E e1 T; P1 E e1 T; WT1 P (E @ [Class C]) e2 T;
           P1 (E @ [Class C]) e2 T; is_class P C |]
        ==> P1 E (try e1 catch(C i) e2) T;
     !!E. P2 E [] [];
     !!E T Ts e es.
        [| WT1 P E e T; P1 E e T; WTs1 P E es Ts; P2 E es Ts |]
        ==> P2 E (e # es) (T # Ts) |]
  ==> (WT1 P xfa xea xda --> P1 xfa xea xda) &
      (WTs1 P xca xba xaa --> P2 xca xba xaa)

lemmas 

  [| WT1 P E (Val v) T; typeof v = ⌊T⌋ ==> Pa |] ==> Pa
  [| WT1 P E (Var i) T; [| i < length E; T = E ! i |] ==> Pa |] ==> Pa
  [| WT1 P E (Cast D e) T;
     !!Da. [| WT1 P E e (Class Da); is_class P D; subcls P D Da | subcls P Da D;
              T = Class D |]
           ==> Pa |]
  ==> Pa
  [| WT1 P E (i:=e) T;
     !!T'. [| i < length E; WT1 P E e T'; widen P T' (E ! i); T = Void |]
           ==> Pa |]
  ==> Pa
  [| WT1 P E {i:U; e} T; [| is_type P U; WT1 P (E @ [U]) e T |] ==> Pa |] ==> Pa
  [| WT1 P E (e1;; e2) T; !!T1. [| WT1 P E e1 T1; WT1 P E e2 T |] ==> Pa |] ==> Pa
  [| WT1 P E (if (e) e1 else e2) T;
     !!T1 T2.
        [| WT1 P E e Boolean; WT1 P E e1 T1; WT1 P E e2 T2;
           widen P T1 T2 | widen P T2 T1; widen P T1 T2 --> T = T2;
           widen P T2 T1 --> T = T1 |]
        ==> Pa |]
  ==> Pa
  [| WT1 P E (while (e) c) T;
     !!Ta. [| WT1 P E e Boolean; WT1 P E c Ta; T = Void |] ==> Pa |]
  ==> Pa
  [| WT1 P E (throw e) T; !!C. [| WT1 P E e (Class C); T = Void |] ==> Pa |]
  ==> Pa
  [| WT1 P E (try e1 catch(C i) e2) T;
     [| WT1 P E e1 T; WT1 P (E @ [Class C]) e2 T; is_class P C |] ==> Pa |]
  ==> Pa
  [| WT1 P E (e\<bullet>F{D}) T;
     !!C. [| WT1 P E e (Class C); P \<turnstile> C sees F:T in D |] ==> Pa |]
  ==> Pa
  [| WT1 P E (e1\<bullet>F{D} := e2) T;
     !!C Ta T'.
        [| WT1 P E e1 (Class C); P \<turnstile> C sees F:Ta in D; WT1 P E e2 T';
           widen P T' Ta; T = Void |]
        ==> Pa |]
  ==> Pa
  [| WT1 P E (e1 «bop» e2) T;
     !!T1 T2.
        [| WT1 P E e1 T1; WT1 P E e2 T2;
           case bop of Eq => (widen P T1 T2 | widen P T2 T1) & T = Boolean
           | Add => T1 = Integer & T2 = Integer & T = Integer |]
        ==> Pa |]
  ==> Pa
  [| WT1 P E (new C) T; [| is_class P C; T = Class C |] ==> Pa |] ==> Pa
  [| WT1 P E (e\<bullet>M(es)) T;
     !!C D Ts Ts' m.
        [| WT1 P E e (Class C); P \<turnstile> C sees M: Ts'->T = m in D;
           WTs1 P E es Ts; widens P Ts Ts' |]
        ==> Pa |]
  ==> Pa
  [| WTs1 P E [] Ts; Ts = [] ==> Pa |] ==> Pa
  [| WTs1 P E (e # es) Ts;
     !!T Tsa. [| WT1 P E e T; WTs1 P E es Tsa; Ts = T # Tsa |] ==> Pa |]
  ==> Pa

lemma WTs1_same_size: 

  WTs1 P E es Ts ==> length es = length Ts

lemma WT1_unique: 

  [| WT1 P E e T1; WT1 P E e T2 |] ==> T1 = T2

and 

  [| WTs1 P E es Ts1; WTs1 P E es Ts2 |] ==> Ts1 = Ts2

lemma WT1_is_type: 

  [| wf_prog p P; WT1 P E e T; set E <= types P |] ==> is_type P T

and 

  [| wf_prog p P; WTs1 P E es Ts |] ==> True

Well-formedness

lemma wf_J1_mdecl: 

  wf_J1_mdecl P C (M, Ts, T, body) ==
  (EX T'. WT1 P (Class C # Ts) body T' & widen P T' T) &
  \<D> body ⌊{..length Ts}⌋ & \<B> body (length Ts + 1)