# Theory Conform

```(*  Title:      Jinja/J/Conform.thy

Author:     David von Oheimb, Tobias Nipkow
*)

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"

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

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

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"