Theory BVConform

(*  Title:      HOL/MicroJava/BV/Correct.thy

    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen

The invariant for the type safety proof.

section ‹BV Type Safety Invariant›

theory BVConform
imports BVSpec "../JVM/JVMExec" "../Common/Conform"

definition confT :: "'c prog  heap  val  ty err  bool" 
    ("_,_  _ :≤ _" [51,51,51,51] 50)
  "P,h  v :≤ E  case E of Err  True | OK T  P,h  v :≤ T"

notation (ASCII)
  confT  ("_,_ |- _ :<=T _" [51,51,51,51] 50)

  confTs :: "'c prog  heap  val list  tyl  bool" 
      ("_,_  _ [:≤] _" [51,51,51,51] 50) where
  "P,h  vs [:≤] Ts  list_all2 (confT P h) vs Ts"

notation (ASCII)
  confTs  ("_,_ |- _ [:<=T] _" [51,51,51,51] 50)

definition conf_f  :: "jvm_prog  heap  tyi  bytecode  frame  bool"
  "conf_f P h  λ(ST,LT) is (stk,loc,C,M,pc).
  P,h  stk [:≤] ST  P,h  loc [:≤] LT  pc < size is"

lemma conf_f_def2:
  "conf_f P h (ST,LT) is (stk,loc,C,M,pc) 
  P,h  stk [:≤] ST  P,h  loc [:≤] LT  pc < size is"
  by (simp add: conf_f_def)

primrec conf_fs :: "[jvm_prog,heap,tyP,mname,nat,ty,frame list]  bool"
  "conf_fs P h Φ M0 n0 T0 [] = True"
| "conf_fs P h Φ M0 n0 T0 (f#frs) =
  (let (stk,loc,C,M,pc) = f in
  (ST LT Ts T mxs mxl0 is xt.
    Φ C M ! pc = Some (ST,LT)  
    (P  C sees M:Ts  T = (mxs,mxl0,is,xt) in C) 
    (D Ts' T' m D'.  
       is!pc = (Invoke M0 n0)  ST!n0 = Class D 
       P  D sees M0:Ts'  T' = m in D'  P  T0  T') 
    conf_f P h (ST, LT) is f  conf_fs P h Φ M (size Ts) T frs))"

definition correct_state :: "[jvm_prog,tyP,jvm_state]  bool"  ("_,_  _ "  [61,0,0] 61)
  "correct_state P Φ  λ(xp,h,frs).
  case xp of
     None  (case frs of
             []  True
             | (f#fs)  P h  
             (let (stk,loc,C,M,pc) = f
              in Ts T mxs mxl0 is xt τ.
                    (P  C sees M:TsT = (mxs,mxl0,is,xt) in C) 
                    Φ C M ! pc = Some τ 
                    conf_f P h τ is f  conf_fs P h Φ M (size Ts) T fs))
  | Some x  frs = []" 

  correct_state  ("_,_ |- _ [ok]"  [61,0,0] 61)

subsection ‹Values and ⊤›

lemma confT_Err [iff]: "P,h  x :≤ Err" 
  by (simp add: confT_def)

lemma confT_OK [iff]:  "P,h  x :≤ OK T = (P,h  x :≤ T)"
  by (simp add: confT_def)

lemma confT_cases:
  "P,h  x :≤ X = (X = Err  (T. X = OK T  P,h  x :≤ T))"
  by (cases X) auto

lemma confT_hext [intro?, trans]:
  " P,h  x :≤ T; h  h'   P,h'  x :≤ T"
  by (cases T) (blast intro: conf_hext)+

lemma confT_widen [intro?, trans]:
  " P,h  x :≤ T; P  T  T'   P,h  x :≤ T'"
  by (cases T', auto intro: conf_widen)

subsection ‹Stack and Registers›

lemmas confTs_Cons1 [iff] = list_all2_Cons1 [of "confT P h"] for P h

lemma confTs_confT_sup:
  " P,h  loc [:≤] LT; n < size LT; LT!n = OK T; P  T  T'  
   P,h  (loc!n) :≤ T'"
  apply (frule list_all2_lengthD)
  apply (drule list_all2_nthD, simp)
  apply simp
  apply (erule conf_widen, assumption+)

lemma confTs_hext [intro?]:
  "P,h  loc [:≤] LT  h  h'  P,h'  loc [:≤] LT"
  by (fast elim: list_all2_mono confT_hext)    

lemma confTs_widen [intro?, trans]:
  "P,h  loc [:≤] LT  P  LT [≤] LT'  P,h  loc [:≤] LT'"
  by (rule list_all2_trans, rule confT_widen)

lemma confTs_map [iff]:
  "vs. (P,h  vs [:≤] map OK Ts) = (P,h  vs [:≤] Ts)"
  by (induct Ts) (auto simp add: list_all2_Cons2)

lemma reg_widen_Err [iff]:
  "LT. (P  replicate n Err [≤] LT) = (LT = replicate n Err)"
  by (induct n) (auto simp add: list_all2_Cons1)
lemma confTs_Err [iff]:
  "P,h  replicate n v [:≤] replicate n Err"
  by (induct n) auto

subsection ‹correct-frames›

lemmas [simp del] = fun_upd_apply

lemma conf_fs_hext:
  "M n Tr. 
   conf_fs P h Φ M n Tr frs; h  h'   conf_fs P h' Φ M n Tr frs"
apply (induct frs)
 apply simp
apply clarify
apply (simp (no_asm_use))
apply clarify
apply (unfold conf_f_def)
apply (simp (no_asm_use))
apply clarify
apply (fast elim!: confs_hext confTs_hext)