Theory WellTypeRT

(*  Title:      Jinja/J/WellTypeRT.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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

theory WellTypeRT
imports WellType
begin

inductive
  WTrt :: "J_prog => heap => env => expr => ty => bool"
  and WTrts :: "J_prog => heap => env => expr list => ty list => bool"
  and WTrt2 :: "[J_prog,env,heap,expr,ty] => bool"
        ("_,_,_ \<turnstile> _ : _"   [51,51,51]50)
  and WTrts2 :: "[J_prog,env,heap,expr list, ty list] => bool"
        ("_,_,_ \<turnstile> _ [:] _" [51,51,51]50)
  for P :: J_prog and h :: heap
where
  
  "P,E,h \<turnstile> e : T ≡ WTrt P h E e T"
| "P,E,h \<turnstile> es[:]Ts ≡ WTrts P h E es Ts"

| 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:
  "typeof⇘h⇙ 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> e⇣1 : T⇣1;  P,E,h \<turnstile> e⇣2 : T⇣2;
    case bop of Eq => T = Boolean
              | Add => T⇣1 = Integer ∧ T⇣2 = Integer ∧ T = Integer |]
   ==> P,E,h \<turnstile> e⇣1 «bop» e⇣2 : T"
*)
| WTrtBinOpEq:
  "[| P,E,h \<turnstile> e⇣1 : T⇣1;  P,E,h \<turnstile> e⇣2 : T⇣2 |]
  ==> P,E,h \<turnstile> e⇣1 «Eq» e⇣2 : Boolean"

| WTrtBinOpAdd:
  "[| P,E,h \<turnstile> e⇣1 : Integer;  P,E,h \<turnstile> e⇣2 : Integer |]
  ==> P,E,h \<turnstile> e⇣1 «Add» e⇣2 : Integer"

| 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•F{D} : T"

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

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

| WTrtFAssNT:
  "[| P,E,h \<turnstile> e⇣1:NT; P,E,h \<turnstile> e⇣2 : T⇣2 |]
  ==> P,E,h \<turnstile> e⇣1•F{D}:=e⇣2 : 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•M(es) : T"

| WTrtCallNT:
  "[| P,E,h \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts |]
  ==> P,E,h \<turnstile> e•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> e⇣1:T⇣1;  P,E,h \<turnstile> e⇣2:T⇣2 |]
  ==> P,E,h \<turnstile> e⇣1;;e⇣2 : T⇣2"

| WTrtCond:
  "[| P,E,h \<turnstile> e : Boolean;  P,E,h \<turnstile> e⇣1:T⇣1;  P,E,h \<turnstile> 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,h \<turnstile> if (e) e⇣1 else e⇣2 : 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 : T⇣r; is_refT T⇣r |] ==>
  P,E,h \<turnstile> throw e : T"

| WTrtTry:
  "[| P,E,h \<turnstile> e⇣1 : T⇣1;  P,E(V \<mapsto> Class C),h \<turnstile> e⇣2 : T⇣2; P \<turnstile> T⇣1 ≤ T⇣2 |]
  ==> P,E,h \<turnstile> try e⇣1 catch(C V) e⇣2 : T⇣2"

-- "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)]
  and WTrt_inducts = WTrt_WTrts.inducts [split_format (complete)]
(*>*)


subsection{*Easy consequences*}

lemma [iff]: "(P,E,h \<turnstile> [] [:] Ts) = (Ts = [])"
(*<*)
apply(rule iffI)
apply (auto elim: WTrts.cases)
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: WTrts.cases)
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: WTrts.cases)
done
(*>*)

lemma [simp]: "∀Ts. (P,E,h \<turnstile> es⇣1 @ es⇣2 [:] Ts) =
  (∃Ts⇣1 Ts⇣2. Ts = Ts⇣1 @ Ts⇣2 ∧ P,E,h \<turnstile> es⇣1 [:] Ts⇣1 & P,E,h \<turnstile> es⇣2[:]Ts⇣2)"
(*<*)
apply(induct_tac es⇣1)
 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 fastforce
done
(*>*)

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

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

lemma [iff]: "P,E,h \<turnstile> e⇣1;;e⇣2 : T⇣2 = (∃T⇣1. P,E,h \<turnstile> e⇣1:T⇣1 ∧ P,E,h \<turnstile> e⇣2:T⇣2)"
(*<*)
apply(rule iffI)
apply (auto elim: WTrt.cases)
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.cases)
done
(*>*)
(*<*)
inductive_cases WTrt_elim_cases[elim!]:
  "P,E,h \<turnstile> v :=e : T"
  "P,E,h \<turnstile> if (e) e⇣1 else e⇣2 : T"
  "P,E,h \<turnstile> while(e) c : T"
  "P,E,h \<turnstile> throw e : T"
  "P,E,h \<turnstile> try e⇣1 catch(C V) e⇣2 : T"
  "P,E,h \<turnstile> Cast D e : T"
  "P,E,h \<turnstile> e•F{D} : T"
  "P,E,h \<turnstile> e•F{D} := v : T"
  "P,E,h \<turnstile> e⇣1 «bop» e⇣2 : T"
  "P,E,h \<turnstile> new C : T"
  "P,E,h \<turnstile> e•M{D}(es) : T"
(*>*)

subsection{*Some interesting lemmas*}

lemma WTrts_Val[simp]:
 "!!Ts. (P,E,h \<turnstile> map Val vs [:] Ts) = (map (typeof⇘h⇙) 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_inducts)
apply(simp add: WTrtNew)
apply(fastforce simp: WTrtCast)
apply(fastforce simp: WTrtVal)
apply(simp add: WTrtVar map_le_def dom_def)
apply(fastforce simp add: WTrtBinOpEq)
apply(fastforce simp add: WTrtBinOpAdd)
apply(force simp: map_le_def)
apply(fastforce simp: WTrtFAcc)
apply(simp add: WTrtFAccNT)
apply(fastforce simp: WTrtFAss)
apply(fastforce simp: WTrtFAssNT)
apply(fastforce simp: WTrtCall)
apply(fastforce simp: WTrtCallNT)
apply(simp add: WTrtNil)
apply(simp add: WTrtCons)
apply(fastforce simp: map_le_def)
apply(fastforce)
apply(fastforce simp: WTrtSeq)
apply(fastforce simp: WTrtWhile)
apply(fastforce simp: WTrtThrow)
apply(auto simp: WTrtTry map_le_def dom_def)
done
(*>*)


lemma WTrt_hext_mono: "P,E,h \<turnstile> e : T ==> h \<unlhd> h' ==> P,E,h' \<turnstile> e : T"
and WTrts_hext_mono: "P,E,h \<turnstile> es [:] Ts ==> h \<unlhd> h' ==> P,E,h' \<turnstile> es [:] Ts"
(*<*)
apply(induct rule: WTrt_inducts)
apply(simp add: WTrtNew)
apply(fastforce simp: WTrtCast)
apply(fastforce simp: WTrtVal dest:hext_typeof_mono)
apply(simp add: WTrtVar)
apply(fastforce simp add: WTrtBinOpEq)
apply(fastforce simp add: WTrtBinOpAdd)
apply(fastforce simp add: WTrtLAss)
apply(fast intro: WTrtFAcc)
apply(simp add: WTrtFAccNT)
apply(fastforce simp: WTrtFAss del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastforce simp: WTrtFAssNT)
apply(fastforce simp: WTrtCall)
apply(fastforce simp: WTrtCallNT)
apply(fastforce)
apply(fastforce simp add: WTrtSeq)
apply(fastforce simp add: WTrtCond)
apply(fastforce simp add: WTrtWhile)
apply(fastforce simp add: WTrtThrow)
apply(fastforce 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_inducts)
apply fast
apply (fast)
apply(fastforce dest:typeof_lit_typeof)
apply(simp)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce simp: WTrtFAcc has_visible_field)
apply(fastforce simp: WTrtFAss dest: has_visible_field)
apply(fastforce simp: WTrtCall)
apply(fastforce)
apply(fastforce)
apply(fastforce simp: WTrtCond)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(simp)
apply(simp)
done
(*>*)


end