Theory WellType

Up to index of Isabelle/HOL/Jinja

theory WellType = Objects + Expr: 
(*  Title:      Jinja/J/WellType.thy
    ID:         $Id: WellType.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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

theory WellType = Objects + Expr:

types 
  env  = "vname => ty"

consts
  WT :: "J_prog => (env × expr      × ty     ) set"
  WTs:: "J_prog => (env × expr list × ty list) set"

(*<*)
syntax (xsymbols)
  WT :: "[J_prog,env, expr     , ty     ] => bool"
         ("_,_ \<turnstile> _ :: _"   [51,51,51]50)
  WTs:: "[J_prog,env, expr list, ty list] => bool"
         ("_,_ \<turnstile> _ [::] _" [51,51,51]50)
(*>*)

translations
  "P,E \<turnstile> e :: T"  ==  "(E,e,T) ∈ WT P"
  "P,E \<turnstile> es [::] Ts"  ==  "(E,es,Ts) ∈ WTs P"
  
inductive "WT P" "WTs P"
intros
  
WTNew:
  "is_class P C  ==>
  P,E \<turnstile> new C :: Class C"

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

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;
     case bop of Eq => (P \<turnstile> T1 ≤ T2 ∨ P \<turnstile> T2 ≤ T1) ∧ T = Boolean
               | Add => T1 = Integer ∧ T2 = Integer ∧ T = Integer |]
  ==> 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"

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

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

WTBlock:
  "[| is_type P T;  P,E(V \<mapsto> T) \<turnstile> e :: T' |]
  ==>  P,E \<turnstile> {V:T; e} :: T'"

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,E \<turnstile> throw e :: Void"

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

-- "well-typed expression lists"

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!] WTNil[iff]

lemmas WT_WTs_induct = WT_WTs.induct[split_format (complete)]
(*>*)

lemma [iff]: "(P,E \<turnstile> [] [::] Ts) = (Ts = [])"
(*<*)
apply(rule iffI)
apply (auto elim: WT_WTs.elims)
done
(*>*)

lemma [iff]: "(P,E \<turnstile> e#es [::] T#Ts) = (P,E \<turnstile> e :: T ∧ P,E \<turnstile> es [::] Ts)"
(*<*)
apply(rule iffI)
apply (auto elim: WT_WTs.elims)
done
(*>*)

lemma [iff]: "(P,E \<turnstile> (e#es) [::] Ts) =
  (∃U Us. Ts = U#Us ∧ P,E \<turnstile> e :: U ∧ P,E \<turnstile> es [::] Us)"
(*<*)
apply(rule iffI)
apply (auto elim: WT_WTs.elims)
done
(*>*)

lemma [iff]: "!!Ts. (P,E \<turnstile> es1 @ es2 [::] Ts) =
  (∃Ts1 Ts2. Ts = Ts1 @ Ts2 ∧ P,E \<turnstile> es1 [::] Ts1 ∧ P,E \<turnstile> es2[::]Ts2)"
(*<*)
apply(induct es1 type:list)
 apply simp
apply clarsimp
apply(erule thin_rl)
apply (rule iffI)
 apply clarsimp
 apply(rule exI)+
 apply(rule conjI)
  prefer 2 apply blast
 apply simp
apply fastsimp
done
(*>*)

lemma [iff]: "P,E \<turnstile> Val v :: T = (typeof v = Some T)"
(*<*)
apply(rule iffI)
apply (auto elim: WT_WTs.elims)
done
(*>*)

lemma [iff]: "P,E \<turnstile> Var V :: T = (E V = Some T)"
(*<*)
apply(rule iffI)
apply (auto elim: WT_WTs.elims)
done
(*>*)

lemma [iff]: "P,E \<turnstile> e1;;e2 :: T2 = (∃T1. P,E \<turnstile> e1::T1 ∧ P,E \<turnstile> e2::T2)"
(*<*)
apply(rule iffI)
apply (auto elim: WT_WTs.elims)
done
(*>*)

lemma [iff]: "(P,E \<turnstile> {V:T; e} :: T') = (is_type P T ∧ P,E(V\<mapsto>T) \<turnstile> e :: T')"
(*<*)
apply(rule iffI)
apply (auto elim: WT_WTs.elims)
done
(*>*)

(*<*)
inductive_cases WT_elim_cases[elim!]:
  "P,E \<turnstile> V :=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\<bullet>F{D} :: T"
  "P,E \<turnstile> a\<bullet>F{D} := v :: T"
  "P,E \<turnstile> e1 «bop» e2 :: T"
  "P,E \<turnstile> new C :: T"
  "P,E \<turnstile> e\<bullet>M(ps) :: T"
(*>*)


lemma wt_env_mono:
  "P,E \<turnstile> e :: T ==> (!!E'. E ⊆m E' ==> P,E' \<turnstile> e :: T)" and 
  "P,E \<turnstile> es [::] Ts ==> (!!E'. E ⊆m E' ==> P,E' \<turnstile> es [::] Ts)"
(*<*)
apply(induct rule: WT_WTs_induct)
apply(simp add: WTNew)
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(fastsimp simp: WTFAcc)
apply(fastsimp simp: WTFAss del:WT_WTs.intros WT_elim_cases)
apply(fastsimp simp: WTCall)
apply(fastsimp simp: map_le_def WTBlock)
apply(fastsimp simp: WTSeq)
apply(fastsimp simp add: WTCond)
apply(fastsimp simp: WTWhile)
apply(fastsimp simp: WTThrow)
apply(fastsimp simp: WTTry map_le_def dom_def)
apply(simp add: WTNil)
apply(simp add: WTCons)
done
(*>*)


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

end
(*>*)

lemmas WT_WTs_induct: 

  [| !!C E. is_class P C ==> P1 E (new C) (Class C);
     !!C D E e.
        [| WT 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 v. E v = ⌊T⌋ ==> P1 E (Var v) T;
     !!E T T1 T2 bop e1 e2.
        [| WT P E e1 T1; P1 E e1 T1; WT 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' V e.
        [| E V = ⌊T⌋; WT P E e T'; P1 E e T'; widen P T' T; V ~= this |]
        ==> P1 E (V:=e) Void;
     !!C D E F T e.
        [| WT 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.
        [| WT P E e1 (Class C); P1 E e1 (Class C); P \<turnstile> C sees F:T in D;
           WT 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' body e es pns.
        [| WT P E e (Class C); P1 E e (Class C);
           P \<turnstile> C sees M: Ts->T = (pns, body) in D; WTs P E es Ts';
           P2 E es Ts'; widens P Ts' Ts |]
        ==> P1 E (e\<bullet>M(es)) T;
     !!E T T' V e.
        [| is_type P T; WT P (E(V |-> T)) e T'; P1 (E(V |-> T)) e T' |]
        ==> P1 E {V:T; e} T';
     !!E T1 T2 e1 e2.
        [| WT P E e1 T1; P1 E e1 T1; WT P E e2 T2; P1 E e2 T2 |]
        ==> P1 E (e1;; e2) T2;
     !!E T T1 T2 e e1 e2.
        [| WT P E e Boolean; P1 E e Boolean; WT P E e1 T1; P1 E e1 T1;
           WT 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.
        [| WT P E e Boolean; P1 E e Boolean; WT P E c T; P1 E c T |]
        ==> P1 E (while (e) c) Void;
     !!C E e. [| WT P E e (Class C); P1 E e (Class C) |] ==> P1 E (throw e) Void;
     !!C E T V e1 e2.
        [| WT P E e1 T; P1 E e1 T; WT P (E(V |-> Class C)) e2 T;
           P1 (E(V |-> Class C)) e2 T; is_class P C |]
        ==> P1 E (try e1 catch(C V) e2) T;
     !!E. P2 E [] [];
     !!E T Ts e es.
        [| WT P E e T; P1 E e T; WTs P E es Ts; P2 E es Ts |]
        ==> P2 E (e # es) (T # Ts) |]
  ==> (WT P xfa xea xda --> P1 xfa xea xda) &
      (WTs P xca xba xaa --> P2 xca xba xaa)

lemma 

  WTs P E [] Ts = (Ts = [])

lemma 

  WTs P E (e # es) (T # Ts) = (WT P E e T & WTs P E es Ts)

lemma 

  WTs P E (e # es) Ts = (EX U Us. Ts = U # Us & WT P E e U & WTs P E es Us)

lemma 

  WTs P E (es1 @ es2) Ts =
  (EX Ts1 Ts2. Ts = Ts1 @ Ts2 & WTs P E es1 Ts1 & WTs P E es2 Ts2)

lemma 

  WT P E (Val v) T = (typeof v = ⌊T⌋)

lemma 

  WT P E (Var V) T = (E V = ⌊T⌋)

lemma 

  WT P E (e1;; e2) T2 = (EX T1. WT P E e1 T1 & WT P E e2 T2)

lemma 

  WT P E {V:T; e} T' = (is_type P T & WT P (E(V |-> T)) e T')

lemmas WT_elim_cases: 

  [| WT P E (V:=e) T;
     !!Ta T'.
        [| E V = ⌊Ta⌋; WT P E e T'; widen P T' Ta; V ~= this; T = Void |]
        ==> Pa |]
  ==> Pa
  [| WT P E (if (e) e1 else e2) T;
     !!T1 T2.
        [| WT P E e Boolean; WT P E e1 T1; WT 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
  [| WT P E (while (e) c) T;
     !!Ta. [| WT P E e Boolean; WT P E c Ta; T = Void |] ==> Pa |]
  ==> Pa
  [| WT P E (throw e) T; !!C. [| WT P E e (Class C); T = Void |] ==> Pa |] ==> Pa
  [| WT P E (try e1 catch(C V) e2) T;
     [| WT P E e1 T; WT P (E(V |-> Class C)) e2 T; is_class P C |] ==> Pa |]
  ==> Pa
  [| WT P E (Cast D e) T;
     !!Da. [| WT P E e (Class Da); is_class P D; subcls P D Da | subcls P Da D;
              T = Class D |]
           ==> Pa |]
  ==> Pa
  [| WT P E (a\<bullet>F{D}) T;
     !!C. [| WT P E a (Class C); P \<turnstile> C sees F:T in D |] ==> Pa |]
  ==> Pa
  [| WT P E (a\<bullet>F{D} := v) T;
     !!C Ta T'.
        [| WT P E a (Class C); P \<turnstile> C sees F:Ta in D; WT P E v T';
           widen P T' Ta; T = Void |]
        ==> Pa |]
  ==> Pa
  [| WT P E (e1 «bop» e2) T;
     !!T1 T2.
        [| WT P E e1 T1; WT 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
  [| WT P E (new C) T; [| is_class P C; T = Class C |] ==> Pa |] ==> Pa
  [| WT P E (e\<bullet>M(ps)) T;
     !!C D Ts Ts' body pns.
        [| WT P E e (Class C); P \<turnstile> C sees M: Ts->T = (pns, body) in D;
           WTs P E ps Ts'; widens P Ts' Ts |]
        ==> Pa |]
  ==> Pa

lemma wt_env_mono: 

  [| WT P E e T; E ⊆m E' |] ==> WT P E' e T

and 

  [| WTs P E es Ts; E ⊆m E' |] ==> WTs P E' es Ts

lemma WT_fv: 

  WT P E e T ==> fv e <= dom E

and 

  WTs P E es Ts ==> fvs es <= dom E