Theory Conform
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⇘h⇙ 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⇘h⇙ 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⇘h⇙ 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