(*  Title:      Jinja/J/Conform.thy

    Author:     David von Oheimb, Tobias Nipkow
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Conformance Relations for Type Soundness Proofs›

theory Conform
imports Exceptions
begin

definition conf :: "'m prog → heap → val → ty → bool"   (‹_,_ ⊨ _ :≤ _›  [51,51,51,51] 50)
where
  "P,h ⊨ v :≤ T ≡
  ∃T'. typeof v = Some T' ∧ P ⊨ T' ≤ T"

definition oconf :: "'m prog → heap → obj → bool"   (‹_,_ ⊨ _ √› [51,51,51] 50)
where
  "P,h ⊨ obj √ ≡
  let (C,fs) = obj in ∀F D T. P ⊨ C has F:T in D ⟶
  (∃v. fs(F,D) = Some v ∧ P,h ⊨ v :≤ T)"

definition hconf :: "'m prog → heap → bool"  (‹_ ⊨ _ √› [51,51] 50)
where
  "P ⊨ h √ ≡
  (∀a obj. h a = Some obj ⟶ P,h ⊨ obj √) ∧ preallocated h"

definition lconf :: "'m prog → heap → (vname ⇀ val) → (vname ⇀ ty) → bool"   (‹_,_ ⊨ _ '(:≤') _› [51,51,51,51] 50)
where
  "P,h ⊨ l (:≤) E ≡
  ∀V v. l V = Some v ⟶ (∃T. E V = Some T ∧ P,h ⊨ v :≤ T)"

abbreviation
  confs :: "'m prog → heap → val list → ty list → bool" 
             (‹_,_ ⊨ _ [:≤] _› [51,51,51,51] 50) where
  "P,h ⊨ vs [:≤] Ts ≡ list_all2 (conf P h) vs Ts"


subsection‹Value conformance ‹:≤››

lemma conf_Null [simp]: "P,h ⊨ Null :≤ T = P ⊨ NT ≤ T"
(*<*)by (simp (no_asm) add: conf_def)(*>*)

lemma typeof_conf[simp]: "typeof v = Some T ==> P,h ⊨ v :≤ T"
(*<*)by (induct v) (auto simp: conf_def)(*>*)

lemma typeof_lit_conf[simp]: "typeof v = Some T ==> P,h ⊨ v :≤ T"
(*<*)by (rule typeof_conf[OF typeof_lit_typeof])(*>*)

lemma defval_conf[simp]: "P,h ⊨ default_val T :≤ T"
(*<*)by (cases T) (auto simp: conf_def)(*>*)

lemma conf_upd_obj: "h a = Some(C,fs) ==> (P,h(a↦(C,fs')) ⊨ x :≤ T) = (P,h ⊨ x :≤ T)"
(*<*)by (rule val.induct) (auto simp:conf_def fun_upd_apply)(*>*)

lemma conf_widen: "P,h ⊨ v :≤ T ==> P ⊨ T ≤ T' ==> P,h ⊨ v :≤ T'"
(*<*)by (induct v) (auto intro: widen_trans simp: conf_def)(*>*)

lemma conf_hext: "h ⊴ h' ==> P,h ⊨ v :≤ T ==> P,h' ⊨ v :≤ T"
(*<*)by (induct v) (auto dest: hext_objD simp: conf_def)(*>*)

lemma conf_ClassD: "P,h ⊨ v :≤ Class C ==>
  v = Null ∨ (∃a obj T. v = Addr a ∧ h a = Some obj ∧ obj_ty obj = T ∧ P ⊨ T ≤ Class C)"
(*<*)by(induct v) (auto simp: conf_def)(*>*)

lemma conf_NT [iff]: "P,h ⊨ v :≤ NT = (v = Null)"
(*<*)by (auto simp add: conf_def)(*>*)

lemma non_npD: "[ v ≠ Null; P,h ⊨ v :≤ Class C ]
  ==> ∃a C' fs. v = Addr a ∧ h a = Some(C',fs) ∧ P ⊨ C' ⪯^* C"
(*<*)by (auto dest: conf_ClassD)(*>*)


subsection‹Value list conformance ‹[:≤]››

lemma confs_widens [trans]: "[P,h ⊨ vs [:≤] Ts; P ⊨ Ts [≤] Ts'] ==> P,h ⊨ vs [:≤] Ts'"
(*<*)by(auto intro: list_all2_trans conf_widen)(*>*)

lemma confs_rev: "P,h ⊨ rev s [:≤] t = (P,h ⊨ s [:≤] rev t)"
(*<*)by (simp add: list_all2_rev1)(*>*)

lemma confs_conv_map:
  "∧Ts'. P,h ⊨ vs [:≤] Ts' = (∃Ts. map typeof vs = map Some Ts ∧ P ⊨ Ts [≤] Ts')"
(*<*)
proof(induct vs)
  case (Cons a vs)
  then show ?case by(case_tac Ts') (auto simp add:conf_def)
qed simp
(*>*)

lemma confs_hext: "P,h ⊨ vs [:≤] Ts ==> h ⊴ h' ==> P,h' ⊨ vs [:≤] Ts"
(*<*)by (erule list_all2_mono, erule conf_hext, assumption)(*>*)

lemma confs_Cons2: "P,h ⊨ xs [:≤] y#ys = (∃z zs. xs = z#zs ∧ P,h ⊨ z :≤ y ∧ P,h ⊨ zs [:≤] ys)"
(*<*)by (rule list_all2_Cons2)(*>*)


subsection "Object conformance"

lemma oconf_hext: "P,h ⊨ obj √ ==> h ⊴ h' ==> P,h' ⊨ obj √"
(*<*)by (fastforce elim:conf_hext simp: oconf_def)(*>*)

lemma oconf_init_fields:
 "P ⊨ C has_fields FDTs ==> P,h ⊨ (C, init_fields FDTs) √"
by(fastforce simp add: has_field_def oconf_def init_fields_def map_of_map
            dest: has_fields_fun)

lemma oconf_fupd [intro?]:
  "[ P ⊨ C has F:T in D; P,h ⊨ v :≤ T; P,h ⊨ (C,fs) √ ]
  ==> P,h ⊨ (C, fs((F,D)↦v)) √"
(*<*)by (auto dest: has_fields_fun simp add: oconf_def has_field_def fun_upd_apply)(*>*)

(*<*)
lemmas oconf_new = oconf_hext [OF _ hext_new]
lemmas oconf_upd_obj = oconf_hext [OF _ hext_upd_obj]
(*>*)

subsection "Heap conformance"

lemma hconfD: "[ P ⊨ h √; h a = Some obj ] ==> P,h ⊨ obj √"
(*<*)by (unfold hconf_def) fast(*>*)

lemma hconf_new: "[ P ⊨ h √; h a = None; P,h ⊨ obj √ ] ==> P ⊨ h(a↦obj) √"
(*<*)by (unfold hconf_def) (auto intro: oconf_new preallocated_new)(*>*)

lemma hconf_upd_obj: "[ P ⊨ h√; h a = Some(C,fs); P,h ⊨ (C,fs')√ ] ==> P ⊨ h(a↦(C,fs'))√"
(*<*)by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)(*>*)


subsection "Local variable conformance"

lemma lconf_hext: "[ P,h ⊨ l (:≤) E; h ⊴ h' ] ==> P,h' ⊨ l (:≤) E"
(*<*)by (unfold lconf_def) (fast elim: conf_hext)(*>*)

lemma lconf_upd:
  "[ P,h ⊨ l (:≤) E; P,h ⊨ v :≤ T; E V = Some T ] ==> P,h ⊨ l(V↦v) (:≤) E"
(*<*)by (unfold lconf_def) auto(*>*)

lemma lconf_empty[iff]: "P,h ⊨ Map.empty (:≤) E"
(*<*)by(simp add:lconf_def)(*>*)

lemma lconf_upd2: "[P,h ⊨ l (:≤) E; P,h ⊨ v :≤ T] ==> P,h ⊨ l(V↦v) (:≤) E(V↦T)"
(*<*)by(simp add:lconf_def)(*>*)


end