header {* \isaheader{Conformance Relations for Type Soundness Proofs} *}
theory Conform
imports ExternalCall
begin
definition conf :: "'m prog => heap => val => ty => bool" ("_,_ \<turnstile> _ :≤ _" [51,51,51,51] 50)
where "P,h \<turnstile> v :≤ T ≡ ∃T'. typeofh v = Some T' ∧ P \<turnstile> T' ≤ T"
definition oconf :: "'m prog => heap => heapobj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
where
"P,h \<turnstile> obj \<surd> ≡
(case obj of Obj C fs => is_class P C ∧ (∀F D T. P \<turnstile> C has F:T in D --> (∃v. fs(F,D) = Some v ∧ P,h \<turnstile> v :≤ T))
| Arr T el => is_type P T ∧ (∀v ∈ set el. 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]: "typeofh 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(Obj C fs) ==> (P,h(a\<mapsto>(Obj 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_upd_arr: "h a = Some(Arr T el) ==> (P,h(a\<mapsto>(Arr T el')) \<turnstile> x :≤ T') = (P,h \<turnstile> x :≤ T')"
apply(unfold conf_def)
apply (rule val.induct)
by (auto simp:fun_upd_apply)
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"
unfolding conf_def
by(induct v)(auto split: heapobj.splits dest: hext_objD hext_arrD)
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)
apply(case_tac a)
apply(simp)
apply(simp)
done
lemma conf_NT [iff]: "P,h \<turnstile> v :≤ NT = (v = Null)"
by (auto simp add: conf_def)
lemma is_IntgI: "P,h \<turnstile> v :≤ Integer ==> is_Intg v"
by (unfold conf_def) auto
lemma is_BoolI: "P,h \<turnstile> v :≤ Boolean ==> is_Bool v"
by (unfold conf_def) auto
lemma is_RefI: "P,h \<turnstile> v :≤ T ==> is_refT T ==> is_Ref v"
apply (cases T)
apply (auto simp add: is_Ref_def dest: conf_ClassD elim: is_refT.cases)
apply(auto simp add: conf_def widen_Array)
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)
by(rule conf_widen)
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 typeofh vs = map Some Ts ∧ P \<turnstile> Ts [≤] Ts')"
apply(induct vs)
apply simp
apply(case_tac Ts')
apply(auto simp add:conf_def)
apply(rule_tac x="T' # Ts" in exI)
apply(simp add: fun_of_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(cases obj)
apply (fastsimp elim:conf_hext)+
done
lemma oconf_init_fields:
"P \<turnstile> C has_fields FDTs ==> P,h \<turnstile> (Obj C (init_fields FDTs)) \<surd>"
apply(frule has_fields_is_class)
by(fastsimp simp add: has_field_def oconf_def init_fields_def map_of_map
dest: has_fields_fun)
lemma oconf_init_arr:
"is_type P U ==> P,h \<turnstile> (Arr U (replicate n (default_val U))) \<surd>"
by(simp add: oconf_def set_replicate_conv_if)
lemma oconf_fupd [intro?]:
"[| P \<turnstile> C has F:T in D; P,h \<turnstile> v :≤ T; P,h \<turnstile> (Obj C fs) \<surd> |]
==> P,h \<turnstile> (Obj 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
lemma oconf_fupd_arr [intro?]:
"[| P,h \<turnstile> v :≤ T; P,h \<turnstile> (Arr T el) \<surd> |]
==> P,h \<turnstile> (Arr T (el[i := v])) \<surd>"
apply(unfold oconf_def)
apply(auto dest: subsetD[OF set_update_subset_insert])
done
lemmas oconf_new = oconf_hext [OF _ hext_new]
lemmas oconf_upd_obj = oconf_hext [OF _ hext_upd_obj]
lemma oconf_upd_arr:
"[| P,h \<turnstile> obj \<surd>; h a = ⌊Arr T el⌋ |] ==> P,h(a \<mapsto> Arr T el') \<turnstile> obj \<surd>"
by(auto simp add: oconf_def conf_upd_arr split: heapobj.split)
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(Obj C fs); P,h \<turnstile> (Obj C fs') \<surd> |] ==> P \<turnstile> h(a\<mapsto>(Obj C fs'))\<surd>"
by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)
lemma hconf_upd_arr: "[| P \<turnstile> h \<surd>; h a = Some(Arr T el); P,h \<turnstile> (Arr T el') \<surd> |] ==> P \<turnstile> h(a\<mapsto>(Arr T el')) \<surd>"
apply(unfold hconf_def)
apply(auto intro: oconf_upd_arr preallocated_upd_arr)
done
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