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


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

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

abbreviation
  confTs :: "'c prog ⇒ heap ⇒ val list ⇒ ty⇩l ⇒ 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 ⇒ ty⇩i ⇒ bytecode ⇒ frame ⇒ bool"
where
  "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,ty⇩P,mname,nat,ty,frame list] ⇒ bool"
where
  "conf_fs P h Φ M⇩0 n⇩0 T⇩0 [] = True"
| "conf_fs P h Φ M⇩0 n⇩0 T⇩0 (f#frs) =
  (let (stk,loc,C,M,pc) = f in
  (∃ST LT Ts T mxs mxl⇩0 is xt.
    Φ C M ! pc = Some (ST,LT) ∧ 
    (P ⊢ C sees M:Ts → T = (mxs,mxl⇩0,is,xt) in C) ∧
    (∃D Ts' T' m D'.  
       is!pc = (Invoke M⇩0 n⇩0) ∧ ST!n⇩0 = Class D ∧
       P ⊢ D sees M⇩0:Ts' → T' = m in D' ∧ P ⊢ T⇩0 ≤ T') ∧
    conf_f P h (ST, LT) is f ∧ conf_fs P h Φ M (size Ts) T frs))"


definition correct_state :: "[jvm_prog,ty⇩P,jvm_state] ⇒ bool"  (‹_,_ ⊢ _ √›  [61,0,0] 61)
where
  "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 mxl⇩0 is xt τ.
                    (P ⊢ C sees M:Ts→T = (mxs,mxl⇩0,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 = []" 

notation
  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+)
  done
(*>*)

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 T⇩r. 
  ⟦ conf_fs P h Φ M n T⇩r frs; h ⊴ h' ⟧ ⟹ conf_fs P h' Φ M n T⇩r 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)
done
(*>*)

end