header {* \isaheader{Conformance Relations for Type Soundness Proofs} *}
theory Conform
imports Exceptions
begin
definition conf :: "'m prog => heap => val => ty => bool" ("_,_ \<turnstile> _ :≤ _" [51,51,51,51] 50)
where
"P,h \<turnstile> v :≤ T ≡
∃T'. typeof⇘h⇙ v = Some T' ∧ P \<turnstile> T' ≤ T"
definition oconf :: "'m prog => heap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
where
"P,h \<turnstile> obj \<surd> ≡
let (C,fs) = obj in ∀F D T. P \<turnstile> C has F:T in D -->
(∃v. fs(F,D) = Some v ∧ P,h \<turnstile> v :≤ T)"
definition hconf :: "'m prog => heap => bool" ("_ \<turnstile> _ \<surd>" [51,51] 50)
where
"P \<turnstile> h \<surd> ≡
(∀a obj. h a = Some obj --> P,h \<turnstile> obj \<surd>) ∧ preallocated h"
definition lconf :: "'m prog => heap => (vname \<rightharpoonup> val) => (vname \<rightharpoonup> ty) => bool" ("_,_ \<turnstile> _ '(:≤') _" [51,51,51,51] 50)
where
"P,h \<turnstile> l (:≤) E ≡
∀V v. l V = Some v --> (∃T. E V = Some T ∧ P,h \<turnstile> v :≤ T)"
abbreviation
confs :: "'m prog => heap => val list => ty list => bool"
("_,_ \<turnstile> _ [:≤] _" [51,51,51,51] 50) where
"P,h \<turnstile> vs [:≤] Ts ≡ list_all2 (conf P h) vs Ts"
section{* Value conformance @{text":≤"} *}
lemma conf_Null [simp]: "P,h \<turnstile> Null :≤ T = P \<turnstile> NT ≤ T"
apply (unfold conf_def)
apply (simp (no_asm))
done
lemma typeof_conf[simp]: "typeof⇘h⇙ v = Some T ==> P,h \<turnstile> v :≤ T"
apply (unfold conf_def)
apply (induct v)
apply auto
done
lemma typeof_lit_conf[simp]: "typeof v = Some T ==> P,h \<turnstile> v :≤ T"
by (rule typeof_conf[OF typeof_lit_typeof])
lemma defval_conf[simp]: "P,h \<turnstile> default_val T :≤ T"
apply (unfold conf_def)
apply (cases T)
apply auto
done
lemma conf_upd_obj: "h a = Some(C,fs) ==> (P,h(a\<mapsto>(C,fs')) \<turnstile> x :≤ T) = (P,h \<turnstile> x :≤ T)"
apply (unfold conf_def)
apply (rule val.induct)
apply (auto simp:fun_upd_apply)
done
lemma conf_widen: "P,h \<turnstile> v :≤ T ==> P \<turnstile> T ≤ T' ==> P,h \<turnstile> v :≤ T'"
apply (unfold conf_def)
apply (induct v)
apply (auto intro: widen_trans)
done
lemma conf_hext: "h \<unlhd> h' ==> P,h \<turnstile> v :≤ T ==> P,h' \<turnstile> v :≤ T"
apply (unfold conf_def)
apply (induct v)
apply (auto dest: hext_objD)
done
lemma conf_ClassD: "P,h \<turnstile> v :≤ Class C ==>
v = Null ∨ (∃a obj T. v = Addr a ∧ h a = Some obj ∧ obj_ty obj = T ∧ P \<turnstile> T ≤ Class C)"
apply (unfold conf_def)
apply(induct "v")
apply(auto)
done
lemma conf_NT [iff]: "P,h \<turnstile> v :≤ NT = (v = Null)"
by (auto simp add: conf_def)
lemma non_npD: "[| v ≠ Null; P,h \<turnstile> v :≤ Class C |]
==> ∃a C' fs. v = Addr a ∧ h a = Some(C',fs) ∧ P \<turnstile> C' \<preceq>⇧* C"
apply (drule conf_ClassD)
apply auto
done
section{* Value list conformance @{text"[:≤]"} *}
lemma confs_widens [trans]: "[|P,h \<turnstile> vs [:≤] Ts; P \<turnstile> Ts [≤] Ts'|] ==> P,h \<turnstile> vs [:≤] Ts'"
apply (rule list_all2_trans)
apply (rule conf_widen, assumption, assumption)
apply assumption
apply assumption
done
lemma confs_rev: "P,h \<turnstile> rev s [:≤] t = (P,h \<turnstile> s [:≤] rev t)"
apply rule
apply (rule subst [OF list_all2_rev])
apply simp
apply (rule subst [OF list_all2_rev])
apply simp
done
lemma confs_conv_map:
"!!Ts'. P,h \<turnstile> vs [:≤] Ts' = (∃Ts. map typeof⇘h⇙ vs = map Some Ts ∧ P \<turnstile> Ts [≤] Ts')"
apply(induct vs)
apply simp
apply(case_tac Ts')
apply(auto simp add:conf_def)
done
lemma confs_hext: "P,h \<turnstile> vs [:≤] Ts ==> h \<unlhd> h' ==> P,h' \<turnstile> vs [:≤] Ts"
by (erule list_all2_mono, erule conf_hext, assumption)
lemma confs_Cons2: "P,h \<turnstile> xs [:≤] y#ys = (∃z zs. xs = z#zs ∧ P,h \<turnstile> z :≤ y ∧ P,h \<turnstile> zs [:≤] ys)"
by (rule list_all2_Cons2)
section "Object conformance"
lemma oconf_hext: "P,h \<turnstile> obj \<surd> ==> h \<unlhd> h' ==> P,h' \<turnstile> obj \<surd>"
apply (unfold oconf_def)
apply (fastforce elim:conf_hext)
done
lemma oconf_init_fields:
"P \<turnstile> C has_fields FDTs ==> P,h \<turnstile> (C, init_fields FDTs) \<surd>"
by(fastforce simp add: has_field_def oconf_def init_fields_def map_of_map
dest: has_fields_fun)
lemma oconf_fupd [intro?]:
"[| P \<turnstile> C has F:T in D; P,h \<turnstile> v :≤ T; P,h \<turnstile> (C,fs) \<surd> |]
==> P,h \<turnstile> (C, fs((F,D)\<mapsto>v)) \<surd>"
apply (unfold oconf_def has_field_def)
apply clarsimp
apply (drule (1) has_fields_fun)
apply (auto simp add: fun_upd_apply)
done
lemmas oconf_new = oconf_hext [OF _ hext_new]
lemmas oconf_upd_obj = oconf_hext [OF _ hext_upd_obj]
section "Heap conformance"
lemma hconfD: "[| P \<turnstile> h \<surd>; h a = Some obj |] ==> P,h \<turnstile> obj \<surd>"
apply (unfold hconf_def)
apply (fast)
done
lemma hconf_new: "[| P \<turnstile> h \<surd>; h a = None; P,h \<turnstile> obj \<surd> |] ==> P \<turnstile> h(a\<mapsto>obj) \<surd>"
by (unfold hconf_def) (auto intro: oconf_new preallocated_new)
lemma hconf_upd_obj: "[| P \<turnstile> h\<surd>; h a = Some(C,fs); P,h \<turnstile> (C,fs')\<surd> |] ==> P \<turnstile> h(a\<mapsto>(C,fs'))\<surd>"
by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)
section "Local variable conformance"
lemma lconf_hext: "[| P,h \<turnstile> l (:≤) E; h \<unlhd> h' |] ==> P,h' \<turnstile> l (:≤) E"
apply (unfold lconf_def)
apply (fast elim: conf_hext)
done
lemma lconf_upd:
"[| P,h \<turnstile> l (:≤) E; P,h \<turnstile> v :≤ T; E V = Some T |] ==> P,h \<turnstile> l(V\<mapsto>v) (:≤) E"
apply (unfold lconf_def)
apply auto
done
lemma lconf_empty[iff]: "P,h \<turnstile> empty (:≤) E"
by(simp add:lconf_def)
lemma lconf_upd2: "[|P,h \<turnstile> l (:≤) E; P,h \<turnstile> v :≤ T|] ==> P,h \<turnstile> l(V\<mapsto>v) (:≤) E(V\<mapsto>T)"
by(simp add:lconf_def)
end