Theory WellTypeRT

(*  Title:       CoreC++
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

    Based on the Jinja theory J/WellTypeRT.thy by Tobias Nipkow 
*)

section ‹Runtime Well-typedness›

theory WellTypeRT imports WellType begin


subsection ‹Run time types›

primrec typeof_h :: "prog  heap  val  ty option" ("_  typeof⇘_") where
  "P  typeofh Unit     = Some Void"
| "P  typeofh Null     = Some NT"
| "P  typeofh (Bool b) = Some Boolean"
| "P  typeofh (Intg i) = Some Integer"
| "P  typeofh (Ref r)  = (case h (the_addr (Ref r)) of None  None 
                            | Some(C,S)  (if Subobjs P C (the_path(Ref r)) then
                                   Some(Class(last(the_path(Ref r))))
                                            else None))"


lemma type_eq_type: "typeof v = Some T  P  typeofh v = Some T"
by(induct v)auto

lemma typeof_Void [simp]: "P  typeofh v = Some Void  v = Unit"
by(induct v,auto split:if_split_asm)

lemma typeof_NT [simp]: "P  typeofh v = Some NT  v = Null"
by(induct v,auto split:if_split_asm)

lemma typeof_Boolean [simp]: "P  typeofh v = Some Boolean  b. v = Bool b"
by(induct v,auto split:if_split_asm)

lemma typeof_Integer [simp]: "P  typeofh v = Some Integer  i. v = Intg i"
by(induct v,auto split:if_split_asm)

lemma typeof_Class_Subo: 
"P  typeofh v = Some (Class C)  
a Cs D S. v = Ref(a,Cs)  h a = Some(D,S)  Subobjs P D Cs  last Cs = C"
by(induct v,auto split:if_split_asm)

subsection ‹The rules›

inductive
  WTrt :: "[prog,env,heap,expr,     ty     ]  bool"
        ("_,_,_  _ : _"   [51,51,51]50)
  and WTrts :: "[prog,env,heap,expr list,ty list]  bool"
        ("_,_,_  _ [:] _" [51,51,51]50)
  for P :: prog
where
  
  WTrtNew:
  "is_class P C   
  P,E,h  new C : Class C"

| WTrtDynCast:
  " P,E,h  e : T; is_refT T; is_class P C 
   P,E,h  Cast C e : Class C"

| WTrtStaticCast:
  " P,E,h  e : T; is_refT T; is_class P C 
   P,E,h  Ce : Class C"

| WTrtVal:
  "P  typeofh v = Some T 
  P,E,h  Val v : T"

| WTrtVar:
  "E V = Some T 
  P,E,h  Var V : T"

| WTrtBinOp:
  " P,E,h  e1 : T1;  P,E,h  e2 : T2;
     case bop of Eq  T = Boolean
               | Add  T1 = Integer  T2 = Integer  T = Integer 
   P,E,h  e1 «bop» e2 : T"

| WTrtLAss:
  " E V = Some T;  P,E,h  e : T'; P  T'  T 
   P,E,h  V:=e : T"

| WTrtFAcc:
"P,E,h  e : Class C; Cs  []; P  C has least F:T via Cs 
   P,E,h  eF{Cs} : T"

| WTrtFAccNT:
  "P,E,h  e : NT  P,E,h  eF{Cs} : T"

| WTrtFAss:
"P,E,h  e1 : Class C; Cs  [];
  P  C has least F:T via Cs; P,E,h  e2 : T'; P  T'  T 
   P,E,h  e1F{Cs}:=e2 : T"

| WTrtFAssNT:
  " P,E,h  e1 : NT; P,E,h  e2 : T'; P  T'  T 
   P,E,h  e1F{Cs}:=e2 : T"

| WTrtCall:
  " P,E,h  e : Class C;  P  C has least M = (Ts,T,m) via Cs;
     P,E,h  es [:] Ts'; P  Ts' [≤] Ts 
   P,E,h  eM(es) : T" 

| WTrtStaticCall:
  " P,E,h  e : Class C'; P  Path C' to C unique;
     P  C has least M = (Ts,T,m) via Cs; 
     P,E,h  es [:] Ts'; P  Ts' [≤] Ts 
   P,E,h  e∙(C::)M(es) : T"

| WTrtCallNT:
  "P,E,h  e : NT; P,E,h  es [:] Ts  P,E,h  Call e Copt M es : T"

| WTrtBlock:
  "P,E(VT),h  e : T'; is_type P T  
  P,E,h  {V:T; e} : T'"

| WTrtSeq:
  " P,E,h  e1 : T1;  P,E,h  e2 : T2     P,E,h  e1;;e2 : T2"

| WTrtCond:
  " P,E,h  e : Boolean;  P,E,h  e1 : T;  P,E,h  e2 : T 
   P,E,h  if (e) e1 else e2 : 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'; is_refT T'  
   P,E,h  throw e : T"


| 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›

inductive_simps [iff]:
  "P,E,h  [] [:] Ts"
  "P,E,h  e#es [:] T#Ts"
  "P,E,h  (e#es) [:] Ts"
  "P,E,h  Val v : T"
  "P,E,h  Var V : T"
  "P,E,h  e1;;e2 : T2"
  "P,E,h  {V:T; e} : T'"


lemma [simp]: "Ts. (P,E,h  es1 @ es2 [:] Ts) =
  (Ts1 Ts2. Ts = Ts1 @ Ts2  P,E,h  es1 [:] Ts1 & P,E,h  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 fastforce
done



inductive_cases WTrt_elim_cases[elim!]:
  "P,E,h  new C : T"
  "P,E,h  Cast C e : T"
  "P,E,h  Ce : T"
  "P,E,h  e1 «bop» e2 : T"
  "P,E,h  V:=e : T"
  "P,E,h  eF{Cs} : T"
  "P,E,h  eF{Cs} := v : T"
  "P,E,h  eM(es) : T"
  "P,E,h  e∙(C::)M(es) : T"
  "P,E,h  if (e) e1 else e2 : T"
  "P,E,h  while(e) c : T"
  "P,E,h  throw e : T"


subsection‹Some interesting lemmas›


lemma WTrts_Val[simp]:
 "Ts. (P,E,h  map Val vs [:] Ts) = (map (λv. (P  typeofh) v) vs = map Some Ts)"

apply(induct vs)
 apply fastforce
apply(case_tac Ts)
 apply simp
apply simp
done



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)"

apply(induct rule: WTrt_inducts)
apply(simp add: WTrtNew)
apply(fastforce simp: WTrtDynCast)
apply(fastforce simp: WTrtStaticCast)
apply(fastforce simp: WTrtVal)
apply(simp add: WTrtVar map_le_def dom_def)
apply(fastforce simp add: WTrtBinOp)
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: WTrtStaticCall)
apply(fastforce simp: WTrtCallNT)
apply(fastforce simp: map_le_def)
apply(fastforce)
apply(fastforce simp: WTrtCond)
apply(fastforce simp: WTrtWhile)
apply(fastforce simp: WTrtThrow)
apply(simp add: WTrtNil)
apply(simp add: WTrtCons)
done


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 thus ?case by (fastforce dest:type_eq_type)
next
  case WTBinOp thus ?case by (fastforce split:bop.splits)
next
  case WTFAcc thus ?case
    by(fastforce intro!:WTrtFAcc dest:Subobjs_nonempty 
                  simp:LeastFieldDecl_def FieldDecls_def)
next
  case WTFAss thus ?case
    by(fastforce intro!:WTrtFAss dest:Subobjs_nonempty
                  simp:LeastFieldDecl_def FieldDecls_def)
next
  case WTCall thus ?case by (fastforce intro:WTrtCall)
qed (auto simp del:fun_upd_apply)


end