(*  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 :≤_\<top> 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 [:≤_\<top>] 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 [:≤_\<top>] 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 [:≤_\<top>] 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₀ n₀ T₀ [] = True"
| "conf_fs P h Φ M₀ n₀ T₀ (f#frs) =
  (let (stk,loc,C,M,pc) = f in
  (∃ST LT Ts T mxs mxl₀ is xt.
    Φ C M ! pc = Some (ST,LT) ∧
    (P ⊨ C sees M:Ts → T = (mxs,mxl₀,is,xt) in C) ∧
    (∃D Ts' T' m D'.
       is!pc = (Invoke M₀ n₀) ∧ ST!n₀ = Class D ∧
       P ⊨ D sees M₀:Ts' → T' = m in D' ∧ P ⊨ T₀ ≤ 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₀ is xt τ.
                    (P ⊨ C sees M:Ts→T = (mxs,mxl₀,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 :≤_\<top> Err" 
  by (simp add: confT_def)

lemma confT_OK [iff]:  "P,h ⊨ x :≤_\<top> OK T = (P,h ⊨ x :≤ T)"
  by (simp add: confT_def)

lemma confT_cases:
  "P,h ⊨ x :≤_\<top> X = (X = Err ∨ (∃T. X = OK T ∧ P,h ⊨ x :≤ T))"
  by (cases X) auto

lemma confT_hext [intro?, trans]:
  "[ P,h ⊨ x :≤_\<top> T; h ⊴ h' ] ==> P,h' ⊨ x :≤_\<top> T"
  by (cases T) (blast intro: conf_hext)+

lemma confT_widen [intro?, trans]:
  "[ P,h ⊨ x :≤_\<top> T; P ⊨ T ≤_\<top> T' ] ==> P,h ⊨ x :≤_\<top> 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 [:≤_\<top>] 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 [:≤_\<top>] LT ==> h ⊴ h' ==> P,h' ⊨ loc [:≤_\<top>] LT"
  by (fast elim: list_all2_mono confT_hext)    

lemma confTs_widen [intro?, trans]:
  "P,h ⊨ loc [:≤_\<top>] LT ==> P ⊨ LT [≤_\<top>] LT' ==> P,h ⊨ loc [:≤_\<top>] LT'"
  by (rule list_all2_trans, rule confT_widen)

lemma confTs_map [iff]:
  "∧vs. (P,h ⊨ vs [:≤_\<top>] 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 [≤_\<top>] LT) = (LT = replicate n Err)"
  by (induct n) (auto simp add: list_all2_Cons1)
    
lemma confTs_Err [iff]:
  "P,h ⊨ replicate n v [:≤_\<top>] 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