Theory WellTypeRT

Up to index of Isabelle/HOL/Jinja

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

header {* \isaheader{Runtime Well-typedness} *}

theory WellTypeRT = WellType:

consts
  WTrt :: "J_prog => (env × heap × expr      × ty     )set"
  WTrts:: "J_prog => (env × heap × expr list × ty list)set"

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

translations
  "P,E,h \<turnstile> e : T"  ==  "(E,h,e,T) ∈ WTrt P"
  "P,E,h \<turnstile> es[:]Ts"  ==  "(E,h,es,Ts) ∈ WTrts P"

inductive "WTrt P" "WTrts P"
intros
  
WTrtNew:
  "is_class P C  ==>
  P,E,h \<turnstile> new C : Class C"

WTrtCast:
  "[| P,E,h \<turnstile> e : T; is_refT T; is_class P C |]
  ==> P,E,h \<turnstile> Cast C e : Class C"

WTrtVal:
  "typeofh v = Some T ==>
  P,E,h \<turnstile> Val v : T"

WTrtVar:
  "E V = Some T  ==>
  P,E,h \<turnstile> Var V : T"

WTrtBinOp:
  "[| P,E,h \<turnstile> e1 : T1;  P,E,h \<turnstile> e2 : T2;
    case bop of Eq => T = Boolean
              | Add => T1 = Integer ∧ T2 = Integer ∧ T = Integer |]
   ==> P,E,h \<turnstile> e1 «bop» e2 : T"

WTrtLAss:
  "[| E V = Some T;  P,E,h \<turnstile> e : T';  P \<turnstile> T' ≤ T |]
   ==> P,E,h \<turnstile> V:=e : Void"

WTrtFAcc:
  "[| P,E,h \<turnstile> e : Class C; P \<turnstile> C has F:T in D |] ==>
  P,E,h \<turnstile> e\<bullet>F{D} : T"

WTrtFAccNT:
  "P,E,h \<turnstile> e : NT ==>
  P,E,h \<turnstile> e\<bullet>F{D} : T"

WTrtFAss:
  "[| P,E,h \<turnstile> e1 : Class C;  P \<turnstile> C has F:T in D; P,E,h \<turnstile> e2 : T2;  P \<turnstile> T2 ≤ T |]
  ==> P,E,h \<turnstile> e1\<bullet>F{D}:=e2 : Void"

WTrtFAssNT:
  "[| P,E,h \<turnstile> e1:NT; P,E,h \<turnstile> e2 : T2 |]
  ==> P,E,h \<turnstile> e1\<bullet>F{D}:=e2 : Void"

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

WTrtCallNT:
  "[| P,E,h \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts |]
  ==> P,E,h \<turnstile> e\<bullet>M(es) : T"

WTrtBlock:
  "P,E(V\<mapsto>T),h \<turnstile> e : T'  ==>
  P,E,h \<turnstile> {V:T; e} : T'"

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

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

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

WTrtThrow:
  "[| P,E,h \<turnstile> e : Tr; is_refT Tr |] ==>
  P,E,h \<turnstile> throw e : T"

WTrtTry:
  "[| P,E,h \<turnstile> e1 : T1;  P,E(V \<mapsto> Class C),h \<turnstile> e2 : T2; P \<turnstile> T1 ≤ T2 |]
  ==> P,E,h \<turnstile> try e1 catch(C V) e2 : T2"

-- "well-typed expression lists"

WTrtNil:
  "P,E,h \<turnstile> [] [:] []"

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

(*<*)
declare
  WTrt_WTrts.intros[intro!]
  WTrtNil[iff]
declare
  WTrtFAcc[rule del] WTrtFAccNT[rule del]
  WTrtFAss[rule del] WTrtFAssNT[rule del]
  WTrtCall[rule del] WTrtCallNT[rule del]

lemmas WTrt_induct = WTrt_WTrts.induct[split_format (complete)]
(*>*)

subsection{*Easy consequences*}

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

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

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

lemma [simp]: "∀Ts. (P,E,h \<turnstile> es1 @ es2 [:] Ts) =
  (∃Ts1 Ts2. Ts = Ts1 @ Ts2 ∧ P,E,h \<turnstile> es1 [:] Ts1 & P,E,h \<turnstile> es2[:]Ts2)"
(*<*)
apply(induct_tac es1)
 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,h \<turnstile> Val v : T = (typeofh v = Some T)"
(*<*)
apply(rule iffI)
apply (auto elim: WTrt_WTrts.elims)
done
(*>*)

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

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

lemma [iff]: "P,E,h \<turnstile> {V:T; e} : T'  =  (P,E(V\<mapsto>T),h \<turnstile> e : T')"
(*<*)
apply(rule iffI)
apply (auto elim: WTrt_WTrts.elims)
done
(*>*)
(*<*)
inductive_cases WTrt_elim_cases[elim!]:
  "P,E,h \<turnstile> v :=e : T"
  "P,E,h \<turnstile> if (e) e1 else e2 : T"
  "P,E,h \<turnstile> while(e) c : T"
  "P,E,h \<turnstile> throw e : T"
  "P,E,h \<turnstile> try e1 catch(C V) e2 : T"
  "P,E,h \<turnstile> Cast D e : T"
  "P,E,h \<turnstile> e\<bullet>F{D} : T"
  "P,E,h \<turnstile> e\<bullet>F{D} := v : T"
  "P,E,h \<turnstile> e1 «bop» e2 : T"
  "P,E,h \<turnstile> new C : T"
  "P,E,h \<turnstile> e\<bullet>M{D}(es) : T"
(*>*)

subsection{*Some interesting lemmas*}

lemma WTrts_Val[simp]:
 "!!Ts. (P,E,h \<turnstile> map Val vs [:] Ts) = (map (typeofh) vs = map Some Ts)"
(*<*)
apply(induct vs)
 apply simp
apply(case_tac Ts)
 apply simp
apply simp
done
(*>*)


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


lemma WTrt_env_mono:
  "P,E,h \<turnstile> e : T ==> (!!E'. E ⊆m E' ==> P,E',h \<turnstile> e : T)" and
  "P,E,h \<turnstile> es [:] Ts ==> (!!E'. E ⊆m E' ==> P,E',h \<turnstile> es [:] Ts)"
(*<*)
apply(induct rule: WTrt_induct)
apply(simp add: WTrtNew)
apply(fastsimp simp: WTrtCast)
apply(fastsimp simp: WTrtVal)
apply(simp add: WTrtVar map_le_def dom_def)
apply(fastsimp simp add: WTrtBinOp)
apply(force simp: map_le_def)
apply(fastsimp simp: WTrtFAcc)
apply(simp add: WTrtFAccNT)
apply(fastsimp simp: WTrtFAss)
apply(fastsimp simp: WTrtFAssNT)
apply(fastsimp simp: WTrtCall)
apply(fastsimp simp: WTrtCallNT)
apply(simp add: WTrtNil)
apply(simp add: WTrtCons)
apply(fastsimp simp: map_le_def)
apply(fastsimp)
apply(fastsimp simp: WTrtSeq)
apply(simp add: WTrtCond)
apply(fastsimp simp: WTrtWhile)
apply(fastsimp simp: WTrtThrow)
apply(auto simp: WTrtTry map_le_def dom_def)
done
(*>*)


lemma WTrt_hext_mono: "P,E,h \<turnstile> e : T ==> (!!h'. h \<unlhd> h' ==> P,E,h' \<turnstile> e : T)"
and WTrts_hext_mono: "P,E,h \<turnstile> es [:] Ts ==> (!!h'. h \<unlhd> h' ==> P,E,h' \<turnstile> es [:] Ts)"
(*<*)
apply(induct rule: WTrt_induct)
apply(simp add: WTrtNew)
apply(fastsimp simp: WTrtCast)
apply(fastsimp simp: WTrtVal dest:hext_typeof_mono)
apply(simp add: WTrtVar)
apply(fastsimp simp add: WTrtBinOp)
apply(fastsimp simp add: WTrtLAss)
apply(fast intro: WTrtFAcc)
apply(simp add: WTrtFAccNT)
apply(fastsimp simp: WTrtFAss del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastsimp simp: WTrtFAssNT)
apply(fastsimp simp: WTrtCall)
apply(fastsimp simp: WTrtCallNT)
apply(fastsimp)
apply(fastsimp simp add: WTrtSeq)
apply(fastsimp simp add: WTrtCond)
apply(fastsimp simp add: WTrtWhile)
apply(fastsimp simp add: WTrtThrow)
apply(fastsimp simp: WTrtTry)
apply(simp add: WTrtNil)
apply(simp add: WTrtCons)
done
(*>*)


lemma WT_implies_WTrt: "P,E \<turnstile> e :: T ==> P,E,h \<turnstile> e : T"
and WTs_implies_WTrts: "P,E \<turnstile> es [::] Ts ==> P,E,h \<turnstile> es [:] Ts"
(*<*)
apply(induct rule: WT_WTs_induct)
apply fast
apply (fast)
apply(fastsimp dest:typeof_lit_typeof)
apply(simp)
apply(fastsimp split:bop.splits)
apply(fastsimp)
apply(fastsimp simp: WTrtFAcc has_visible_field)
apply(fastsimp simp: WTrtFAss dest: has_visible_field)
apply(fastsimp simp: WTrtCall)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(simp)
apply(simp)
done
(*>*)


end

lemmas WTrt_induct: 

  [| !!C E h. is_class P C ==> P1 E h (new C) (Class C);
     !!C E T e h.
        [| WTrt P E h e T; P1 E h e T; is_refT T; is_class P C |]
        ==> P1 E h (Cast C e) (Class C);
     !!E T h v. typeofh v = ⌊T⌋ ==> P1 E h (Val v) T;
     !!E T V h. E V = ⌊T⌋ ==> P1 E h (Var V) T;
     !!E T T1 T2 bop e1 e2 h.
        [| WTrt P E h e1 T1; P1 E h e1 T1; WTrt P E h e2 T2; P1 E h e2 T2;
           case bop of Eq => T = Boolean
           | Add => T1 = Integer & T2 = Integer & T = Integer |]
        ==> P1 E h (e1 «bop» e2) T;
     !!E T T' V e h.
        [| E V = ⌊T⌋; WTrt P E h e T'; P1 E h e T'; widen P T' T |]
        ==> P1 E h (V:=e) Void;
     !!C D E F T e h.
        [| WTrt P E h e (Class C); P1 E h e (Class C);
           P \<turnstile> C has F:T in D |]
        ==> P1 E h (e\<bullet>F{D}) T;
     !!D E F T e h.
        [| WTrt P E h e NT; P1 E h e NT |] ==> P1 E h (e\<bullet>F{D}) T;
     !!C D E F T T2 e1 e2 h.
        [| WTrt P E h e1 (Class C); P1 E h e1 (Class C);
           P \<turnstile> C has F:T in D; WTrt P E h e2 T2; P1 E h e2 T2;
           widen P T2 T |]
        ==> P1 E h (e1\<bullet>F{D} := e2) Void;
     !!D E F T2 e1 e2 h.
        [| WTrt P E h e1 NT; P1 E h e1 NT; WTrt P E h e2 T2; P1 E h e2 T2 |]
        ==> P1 E h (e1\<bullet>F{D} := e2) Void;
     !!C D E M T Ts Ts' body e es h pns.
        [| WTrt P E h e (Class C); P1 E h e (Class C);
           P \<turnstile> C sees M: Ts->T = (pns, body) in D; WTrts P E h es Ts';
           P2 E h es Ts'; widens P Ts' Ts |]
        ==> P1 E h (e\<bullet>M(es)) T;
     !!E M T Ts e es h.
        [| WTrt P E h e NT; P1 E h e NT; WTrts P E h es Ts; P2 E h es Ts |]
        ==> P1 E h (e\<bullet>M(es)) T;
     !!E T T' V e h.
        [| WTrt P (E(V |-> T)) h e T'; P1 (E(V |-> T)) h e T' |]
        ==> P1 E h {V:T; e} T';
     !!E T1 T2 e1 e2 h.
        [| WTrt P E h e1 T1; P1 E h e1 T1; WTrt P E h e2 T2; P1 E h e2 T2 |]
        ==> P1 E h (e1;; e2) T2;
     !!E T T1 T2 e e1 e2 h.
        [| WTrt P E h e Boolean; P1 E h e Boolean; WTrt P E h e1 T1; P1 E h e1 T1;
           WTrt P E h e2 T2; P1 E h e2 T2; widen P T1 T2 | widen P T2 T1;
           widen P T1 T2 --> T = T2; widen P T2 T1 --> T = T1 |]
        ==> P1 E h (if (e) e1 else e2) T;
     !!E T c e h.
        [| WTrt P E h e Boolean; P1 E h e Boolean; WTrt P E h c T; P1 E h c T |]
        ==> P1 E h (while (e) c) Void;
     !!E T Tr e h.
        [| WTrt P E h e Tr; P1 E h e Tr; is_refT Tr |] ==> P1 E h (throw e) T;
     !!C E T1 T2 V e1 e2 h.
        [| WTrt P E h e1 T1; P1 E h e1 T1; WTrt P (E(V |-> Class C)) h e2 T2;
           P1 (E(V |-> Class C)) h e2 T2; widen P T1 T2 |]
        ==> P1 E h (try e1 catch(C V) e2) T2;
     !!E h. P2 E h [] [];
     !!E T Ts e es h.
        [| WTrt P E h e T; P1 E h e T; WTrts P E h es Ts; P2 E h es Ts |]
        ==> P2 E h (e # es) (T # Ts) |]
  ==> (WTrt P xha xga xfa xea --> P1 xha xga xfa xea) &
      (WTrts P xda xca xba xaa --> P2 xda xca xba xaa)

Easy consequences

lemma 

  WTrts P E h [] Ts = (Ts = [])

lemma 

  WTrts P E h (e # es) (T # Ts) = (WTrt P E h e T & WTrts P E h es Ts)

lemma 

  WTrts P E h (e # es) Ts =
  (EX U Us. Ts = U # Us & WTrt P E h e U & WTrts P E h es Us)

lemma 

  ALL Ts.
     WTrts P E h (es1 @ es2) Ts =
     (EX Ts1 Ts2. Ts = Ts1 @ Ts2 & WTrts P E h es1 Ts1 & WTrts P E h es2 Ts2)

lemma 

  WTrt P E h (Val v) T = (typeofh v = ⌊T⌋)

lemma 

  WTrt P E h (Var v) T = (E v = ⌊T⌋)

lemma 

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

lemma 

  WTrt P E h {V:T; e} T' = WTrt P (E(V |-> T)) h e T'

lemmas WTrt_elim_cases: 

  [| WTrt P E h (v:=e) T;
     !!Ta T'. [| E v = ⌊Ta⌋; WTrt P E h e T'; widen P T' Ta; T = Void |] ==> Pa |]
  ==> Pa
  [| WTrt P E h (if (e) e1 else e2) T;
     !!T1 T2.
        [| WTrt P E h e Boolean; WTrt P E h e1 T1; WTrt P E h e2 T2;
           widen P T1 T2 | widen P T2 T1; widen P T1 T2 --> T = T2;
           widen P T2 T1 --> T = T1 |]
        ==> Pa |]
  ==> Pa
  [| WTrt P E h (while (e) c) T;
     !!Ta. [| WTrt P E h e Boolean; WTrt P E h c Ta; T = Void |] ==> Pa |]
  ==> Pa
  [| WTrt P E h (throw e) T; !!Tr. [| WTrt P E h e Tr; is_refT Tr |] ==> Pa |]
  ==> Pa
  [| WTrt P E h (try e1 catch(C V) e2) T;
     !!T1. [| WTrt P E h e1 T1; WTrt P (E(V |-> Class C)) h e2 T; widen P T1 T |]
           ==> Pa |]
  ==> Pa
  [| WTrt P E h (Cast D e) T;
     !!Ta. [| WTrt P E h e Ta; is_refT Ta; is_class P D; T = Class D |] ==> Pa |]
  ==> Pa
  [| WTrt P E h (e\<bullet>F{D}) T;
     !!C. [| WTrt P E h e (Class C); P \<turnstile> C has F:T in D |] ==> Pa;
     WTrt P E h e NT ==> Pa |]
  ==> Pa
  [| WTrt P E h (e\<bullet>F{D} := v) T;
     !!C Ta T2.
        [| WTrt P E h e (Class C); P \<turnstile> C has F:Ta in D;
           WTrt P E h v T2; widen P T2 Ta; T = Void |]
        ==> Pa;
     !!T2. [| WTrt P E h e NT; WTrt P E h v T2; T = Void |] ==> Pa |]
  ==> Pa
  [| WTrt P E h (e1 «bop» e2) T;
     !!T1 T2.
        [| WTrt P E h e1 T1; WTrt P E h e2 T2;
           case bop of Eq => T = Boolean
           | Add => T1 = Integer & T2 = Integer & T = Integer |]
        ==> Pa |]
  ==> Pa
  [| WTrt P E h (new C) T; [| is_class P C; T = Class C |] ==> Pa |] ==> Pa
  [| WTrt P E h (e\<bullet>M {D}(es)) T;
     !!C Da Ts Ts' body pns.
        [| WTrt P E h e (Class C);
           P \<turnstile> C sees M {D}: Ts->T = (pns, body) in Da;
           WTrts P E h es Ts'; widens P Ts' Ts |]
        ==> Pa;
     !!Ts. [| WTrt P E h e NT; WTrts P E h es Ts |] ==> Pa |]
  ==> Pa

Some interesting lemmas

lemma WTrts_Val: 

  WTrts P E h (map Val vs) Ts = (map typeofh vs = map Some Ts)

lemma WTrts_same_length: 

  WTrts P E h es Ts ==> length es = length Ts

lemma WTrt_env_mono: 

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

and 

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

lemma WTrt_hext_mono: 

  [| WTrt P E h e T; h \<unlhd> h' |] ==> WTrt P E h' e T

and WTrts_hext_mono: 

  [| WTrts P E h es Ts; h \<unlhd> h' |] ==> WTrts P E h' es Ts

lemma WT_implies_WTrt: 

  WT P E e T ==> WTrt P E h e T

and WTs_implies_WTrts: 

  WTs P E es Ts ==> WTrts P E h es Ts