Theory WellTypeRT

(*  Title:      Jinja/J/WellTypeRT.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

section ‹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"
        ("_,_,_ ⊢ _ : _"   [51,51,51]50)
  and WTrts2 :: "[J_prog,env,heap,expr list, ty list] ⇒ bool"
        ("_,_,_ ⊢ _ [:] _" [51,51,51]50)
  for P :: J_prog and h :: heap
where
  
  "P,E,h ⊢ e : T ≡ WTrt P h E e T"
| "P,E,h ⊢ es[:]Ts ≡ WTrts P h E es Ts"

| WTrtNew:
  "is_class P C  ⟹
  P,E,h ⊢ new C : Class C"

| WTrtCast:
  "⟦ P,E,h ⊢ e : T; is_refT T; is_class P C ⟧
  ⟹ P,E,h ⊢ Cast C e : Class C"

| WTrtVal:
  "typeof⇘h⇙ v = Some T ⟹
  P,E,h ⊢ Val v : T"

| WTrtVar:
  "E V = Some T  ⟹
  P,E,h ⊢ Var V : T"
(*
WTrtBinOp:
  "⟦ P,E,h ⊢ e⇩1 : T⇩1;  P,E,h ⊢ e⇩2 : T⇩2;
    case bop of Eq ⇒ T = Boolean
              | Add ⇒ T⇩1 = Integer ∧ T⇩2 = Integer ∧ T = Integer ⟧
   ⟹ P,E,h ⊢ e⇩1 «bop» e⇩2 : T"
*)
| WTrtBinOpEq:
  "⟦ P,E,h ⊢ e⇩1 : T⇩1;  P,E,h ⊢ e⇩2 : T⇩2 ⟧
  ⟹ P,E,h ⊢ e⇩1 «Eq» e⇩2 : Boolean"

| WTrtBinOpAdd:
  "⟦ P,E,h ⊢ e⇩1 : Integer;  P,E,h ⊢ e⇩2 : Integer ⟧
  ⟹ P,E,h ⊢ e⇩1 «Add» e⇩2 : Integer"

| WTrtLAss:
  "⟦ E V = Some T;  P,E,h ⊢ e : T';  P ⊢ T' ≤ T ⟧
   ⟹ P,E,h ⊢ V:=e : Void"

| WTrtFAcc:
  "⟦ P,E,h ⊢ e : Class C; P ⊢ C has F:T in D ⟧ ⟹
  P,E,h ⊢ e∙F{D} : T"

| WTrtFAccNT:
  "P,E,h ⊢ e : NT ⟹
  P,E,h ⊢ e∙F{D} : T"

| WTrtFAss:
  "⟦ P,E,h ⊢ e⇩1 : Class C;  P ⊢ C has F:T in D; P,E,h ⊢ e⇩2 : T⇩2;  P ⊢ T⇩2 ≤ T ⟧
  ⟹ P,E,h ⊢ e⇩1∙F{D}:=e⇩2 : Void"

| WTrtFAssNT:
  "⟦ P,E,h ⊢ e⇩1:NT; P,E,h ⊢ e⇩2 : T⇩2 ⟧
  ⟹ P,E,h ⊢ e⇩1∙F{D}:=e⇩2 : Void"

| WTrtCall:
  "⟦ P,E,h ⊢ e : Class C; P ⊢ C sees M:Ts → T = (pns,body) in D;
     P,E,h ⊢ es [:] Ts'; P ⊢ Ts' [≤] Ts ⟧
  ⟹ P,E,h ⊢ e∙M(es) : T"

| WTrtCallNT:
  "⟦ P,E,h ⊢ e : NT; P,E,h ⊢ es [:] Ts ⟧
  ⟹ P,E,h ⊢ e∙M(es) : T"

| WTrtBlock:
  "P,E(V↦T),h ⊢ e : T'  ⟹
  P,E,h ⊢ {V:T; e} : T'"

| WTrtSeq:
  "⟦ P,E,h ⊢ e⇩1:T⇩1;  P,E,h ⊢ e⇩2:T⇩2 ⟧
  ⟹ P,E,h ⊢ e⇩1;;e⇩2 : T⇩2"

| WTrtCond:
  "⟦ P,E,h ⊢ e : Boolean;  P,E,h ⊢ e⇩1:T⇩1;  P,E,h ⊢ e⇩2:T⇩2;
     P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1; P ⊢ T⇩1 ≤ T⇩2 ⟶ T = T⇩2; P ⊢ T⇩2 ≤ T⇩1 ⟶ T = T⇩1 ⟧
  ⟹ P,E,h ⊢ if (e) e⇩1 else e⇩2 : T"

| WTrtWhile:
  "⟦ P,E,h ⊢ e : Boolean;  P,E,h ⊢ c:T ⟧
  ⟹  P,E,h ⊢ while(e) c : Void"

| WTrtThrow:
  "⟦ P,E,h ⊢ e : T⇩r; is_refT T⇩r ⟧ ⟹
  P,E,h ⊢ throw e : T"

| WTrtTry:
  "⟦ P,E,h ⊢ e⇩1 : T⇩1;  P,E(V ↦ Class C),h ⊢ e⇩2 : T⇩2; P ⊢ T⇩1 ≤ T⇩2 ⟧
  ⟹ P,E,h ⊢ try e⇩1 catch(C V) e⇩2 : T⇩2"

― ‹well-typed expression lists›

| WTrtNil:
  "P,E,h ⊢ [] [:] []"

| WTrtCons:
  "⟦ P,E,h ⊢ e : T;  P,E,h ⊢ es [:] Ts ⟧
  ⟹  P,E,h ⊢ 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 ⊢ [] [:] Ts) = (Ts = [])"
(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)

lemma [iff]: "(P,E,h ⊢ e#es [:] T#Ts) = (P,E,h ⊢ e : T ∧ P,E,h ⊢ es [:] Ts)"
(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)

lemma [iff]: "(P,E,h ⊢ (e#es) [:] Ts) =
  (∃U Us. Ts = U#Us ∧ P,E,h ⊢ e : U ∧ P,E,h ⊢ es [:] Us)"
(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)

lemma [simp]: "∀Ts. (P,E,h ⊢ es⇩1 @ es⇩2 [:] Ts) =
  (∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧ P,E,h ⊢ es⇩1 [:] Ts⇩1 & P,E,h ⊢ es⇩2[:]Ts⇩2)"
(*<*)
proof(induct es⇩1)
  case (Cons a list)
  let ?lhs = "λTs. (∃U Us. Ts = U # Us ∧ P,E,h ⊢ a : U ∧
        (∃Ts⇩1 Ts⇩2. Us = Ts⇩1 @ Ts⇩2 ∧ P,E,h ⊢ list [:] Ts⇩1 ∧ P,E,h ⊢ es⇩2 [:] Ts⇩2))"
  let ?rhs = "λTs. (∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧
        (∃U Us. Ts⇩1 = U # Us ∧ P,E,h ⊢ a : U ∧ P,E,h ⊢ list [:] Us) ∧ P,E,h ⊢ es⇩2 [:] Ts⇩2)"
  { fix Ts assume "?lhs Ts"
    then have "?rhs Ts" by (auto intro: Cons_eq_appendI)
  }
  moreover {
    fix Ts assume "?rhs Ts"
    then have "?lhs Ts" by fastforce
  }
  ultimately have "⋀Ts. ?lhs Ts = ?rhs Ts" by(rule iffI)
  then show ?case by (clarsimp simp: Cons)
qed simp
(*>*)

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

lemma [iff]: "P,E,h ⊢ Var v : T = (E v = Some T)"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

lemma [iff]: "P,E,h ⊢ e⇩1;;e⇩2 : T⇩2 = (∃T⇩1. P,E,h ⊢ e⇩1:T⇩1 ∧ P,E,h ⊢ e⇩2:T⇩2)"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

lemma [iff]: "P,E,h ⊢ {V:T; e} : T'  =  (P,E(V↦T),h ⊢ e : T')"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

(*<*)
inductive_cases WTrt_elim_cases[elim!]:
  "P,E,h ⊢ v :=e : T"
  "P,E,h ⊢ if (e) e⇩1 else e⇩2 : T"
  "P,E,h ⊢ while(e) c : T"
  "P,E,h ⊢ throw e : T"
  "P,E,h ⊢ try e⇩1 catch(C V) e⇩2 : T"
  "P,E,h ⊢ Cast D e : T"
  "P,E,h ⊢ e∙F{D} : T"
  "P,E,h ⊢ e∙F{D} := v : T"
  "P,E,h ⊢ e⇩1 «bop» e⇩2 : T"
  "P,E,h ⊢ new C : T"
  "P,E,h ⊢ e∙M{D}(es) : T"
(*>*)

subsection‹Some interesting lemmas›

lemma WTrts_Val[simp]:
 "⋀Ts. (P,E,h ⊢ map Val vs [:] Ts) = (map (typeof⇘h⇙) vs = map Some Ts)"
(*<*)
proof(induct vs)
  case (Cons a vs)
  then show ?case by(case_tac Ts; simp)
qed simp
(*>*)


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


lemma WTrt_env_mono:
  "P,E,h ⊢ e : T ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E',h ⊢ e : T)" and
  "P,E,h ⊢ es [:] Ts ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E',h ⊢ es [:] Ts)"
(*<*)
proof(induct rule: WTrt_inducts)
  case WTrtVar then show ?case by(simp add: map_le_def dom_def)
next
  case WTrtLAss then show ?case by(force simp:map_le_def)
qed(fastforce intro: WTrt_WTrts.intros)+
(*>*)


lemma WTrt_hext_mono: "P,E,h ⊢ e : T ⟹ h ⊴ h' ⟹ P,E,h' ⊢ e : T"
and WTrts_hext_mono: "P,E,h ⊢ es [:] Ts ⟹ h ⊴ h' ⟹ P,E,h' ⊢ es [:] Ts"
(*<*)
proof(induct rule: WTrt_inducts)
  case WTrtVal then show ?case by(simp add: hext_typeof_mono)
qed(fastforce intro: WTrt_WTrts.intros)+
(*>*)


lemma WT_implies_WTrt: "P,E ⊢ e :: T ⟹ P,E,h ⊢ e : T"
and WTs_implies_WTrts: "P,E ⊢ es [::] Ts ⟹ P,E,h ⊢ es [:] Ts"
(*<*)
proof(induct rule: WT_WTs_inducts)
  case WTVal then show ?case by(fastforce dest: typeof_lit_typeof)
next
  case WTFAcc
  then show ?case by(fastforce simp: WTrtFAcc has_visible_field)
next
  case WTFAss
  then show ?case by(fastforce simp: WTrtFAss dest: has_visible_field)
qed(fastforce intro: WTrt_WTrts.intros)+
(*>*)


end