header {* \isaheader{Conformance Relations for Proofs} *}
theory Conform imports Exceptions WellTypeRT begin
consts
conf :: "prog => heap => val => ty => bool" ("_,_ \<turnstile> _ :≤ _" [51,51,51,51] 50)
primrec
"P,h \<turnstile> v :≤ Void = (P \<turnstile> typeofh v = Some Void)"
"P,h \<turnstile> v :≤ Boolean = (P \<turnstile> typeofh v = Some Boolean)"
"P,h \<turnstile> v :≤ Integer = (P \<turnstile> typeofh v = Some Integer)"
"P,h \<turnstile> v :≤ NT = (P \<turnstile> typeofh v = Some NT)"
"P,h \<turnstile> v :≤ (Class C) = (P \<turnstile> typeofh v = Some(Class C) ∨ P \<turnstile> typeofh v = Some NT)"
constdefs
fconf :: "prog => heap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool" ("_,_ \<turnstile> _ '(:≤') _" [51,51,51,51] 50)
"P,h \<turnstile> vm (:≤) Tm ≡
∀FD T. Tm FD = Some T --> (∃v. vm FD = Some v ∧ P,h \<turnstile> v :≤ T)"
oconf :: "prog => heap => obj => bool" ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
"P,h \<turnstile> obj \<surd> ≡ let (C,S) = obj in
(∀Cs. Subobjs P C Cs --> (∃!fs'. (Cs,fs') ∈ S)) ∧
(∀Cs fs'. (Cs,fs') ∈ S --> Subobjs P C Cs ∧
(∃fs Bs ms. class P (last Cs) = Some (Bs,fs,ms) ∧
P,h \<turnstile> fs' (:≤) map_of fs))"
hconf :: "prog => heap => bool" ("_ \<turnstile> _ \<surd>" [51,51] 50)
"P \<turnstile> h \<surd> ≡
(∀a obj. h a = Some obj --> P,h \<turnstile> obj \<surd>) ∧ preallocated h"
lconf :: "prog => heap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool" ("_,_ \<turnstile> _ '(:≤')w _" [51,51,51,51] 50)
"P,h \<turnstile> vm (:≤)w Tm ≡
∀V v. vm V = Some v --> (∃T. Tm V = Some T ∧ P,h \<turnstile> v :≤ T)"
abbreviation
confs :: "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"
by(cases T) simp_all
lemma typeof_conf[simp]: "P \<turnstile> typeofh v = Some T ==> P,h \<turnstile> v :≤ T"
by (cases T) auto
lemma typeof_lit_conf[simp]: "typeof v = Some T ==> P,h \<turnstile> v :≤ T"
by (rule typeof_conf[OF type_eq_type])
lemma defval_conf[simp]: "is_type P T ==> P,h \<turnstile> default_val T :≤ T"
by(cases T) auto
lemma typeof_notclass_heap:
"∀C. T ≠ Class C ==> (P \<turnstile> typeofh v = Some T) = (P \<turnstile> typeofh' v = Some T)"
by(cases T)(auto dest:typeof_Void typeof_NT typeof_Boolean typeof_Integer)
lemma assumes h:"h a = Some(C,S)"
shows conf_upd_obj: "(P,h(a\<mapsto>(C,S')) \<turnstile> v :≤ T) = (P,h \<turnstile> v :≤ T)"
proof(cases T)
case Void
hence "(P \<turnstile> typeofh(a\<mapsto>(C,S')) v = Some T) = (P \<turnstile> typeofh v = Some T)"
by(fastsimp intro!:typeof_notclass_heap)
with Void show ?thesis by simp
next
case Boolean
hence "(P \<turnstile> typeofh(a\<mapsto>(C,S')) v = Some T) = (P \<turnstile> typeofh v = Some T)"
by(fastsimp intro!:typeof_notclass_heap)
with Boolean show ?thesis by simp
next
case Integer
hence "(P \<turnstile> typeofh(a\<mapsto>(C,S')) v = Some T) = (P \<turnstile> typeofh v = Some T)"
by(fastsimp intro!:typeof_notclass_heap)
with Integer show ?thesis by simp
next
case NT
hence "(P \<turnstile> typeofh(a\<mapsto>(C,S')) v = Some T) = (P \<turnstile> typeofh v = Some T)"
by(fastsimp intro!:typeof_notclass_heap)
with NT show ?thesis by simp
next
case (Class C')
{ assume "P \<turnstile> typeofh(a \<mapsto> (C, S')) v = Some(Class C')"
with h have "P \<turnstile> typeofh v = Some(Class C')"
by (cases v) (auto split:split_if_asm) }
hence 1:"P \<turnstile> typeofh(a \<mapsto> (C, S')) v = Some(Class C') ==>
P \<turnstile> typeofh v = Some(Class C')" by simp
{ assume type:"P \<turnstile> typeofh(a \<mapsto> (C, S')) v = Some NT"
and typenot:"P \<turnstile> typeofh v ≠ Some NT"
have "∀C. NT ≠ Class C" by simp
with type have "P \<turnstile> typeofh v = Some NT" by(fastsimp dest:typeof_notclass_heap)
with typenot have "P \<turnstile> typeofh v = Some(Class C')" by simp }
hence 2:"[|P \<turnstile> typeofh(a \<mapsto> (C, S')) v = Some NT; P \<turnstile> typeofh v ≠ Some NT|] ==>
P \<turnstile> typeofh v = Some(Class C')" by simp
{ assume "P \<turnstile> typeofh v = Some(Class C')"
with h have "P \<turnstile> typeofh(a \<mapsto> (C, S')) v = Some(Class C')"
by (cases v) (auto split:split_if_asm) }
hence 3:"P \<turnstile> typeofh v = Some(Class C') ==>
P \<turnstile> typeofh(a \<mapsto> (C, S')) v = Some(Class C')" by simp
{ assume typenot:"P \<turnstile> typeofh(a \<mapsto> (C, S')) v ≠ Some NT"
and type:"P \<turnstile> typeofh v = Some NT"
have "∀C. NT ≠ Class C" by simp
with type have "P \<turnstile> typeofh(a \<mapsto> (C, S')) v = Some NT"
by(fastsimp dest:typeof_notclass_heap)
with typenot have "P \<turnstile> typeofh(a \<mapsto> (C, S')) v = Some(Class C')" by simp }
hence 4:"[|P \<turnstile> typeofh(a \<mapsto> (C, S')) v ≠ Some NT; P \<turnstile> typeofh v = Some NT|] ==>
P \<turnstile> typeofh(a \<mapsto> (C, S')) v = Some(Class C')" by simp
from Class show ?thesis by (auto intro:1 2 3 4)
qed
lemma conf_NT [iff]: "P,h \<turnstile> v :≤ NT = (v = Null)"
by fastsimp
section{* Value list conformance @{text"[:≤]"} *}
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_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{* Field conformance @{text"(:≤)"} *}
lemma fconf_init_fields:
"class P C = Some(Bs,fs,ms) ==> P,h \<turnstile> init_class_fieldmap P C (:≤) map_of fs"
apply(unfold fconf_def init_class_fieldmap_def)
apply clarsimp
apply (rule exI)
apply (rule conjI)
apply (simp add:map_of_map)
apply(case_tac T)
apply simp_all
done
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_Subobjs:
"[|h a = Some(C,S); (Cs, fs) ∈ S; P \<turnstile> h \<surd>|] ==> Subobjs P C Cs"
apply (unfold hconf_def)
apply clarsimp
apply (erule_tac x="a" in allE)
apply (erule_tac x="C" in allE)
apply (erule_tac x="S" in allE)
apply clarsimp
apply (unfold oconf_def)
apply fastsimp
done
section {*Local variable conformance*}
lemma lconf_upd:
"[| P,h \<turnstile> l (:≤)w E; P,h \<turnstile> v :≤ T; E V = Some T |] ==> P,h \<turnstile> l(V\<mapsto>v) (:≤)w E"
apply (unfold lconf_def)
apply auto
done
lemma lconf_empty[iff]: "P,h \<turnstile> empty (:≤)w E"
by(simp add:lconf_def)
lemma lconf_upd2: "[|P,h \<turnstile> l (:≤)w E; P,h \<turnstile> v :≤ T|] ==> P,h \<turnstile> l(V\<mapsto>v) (:≤)w E(V\<mapsto>T)"
by(simp add:lconf_def)
section{* Environment conformance *}
constdefs
envconf :: "prog => env => bool" ("_ \<turnstile> _ \<surd>" [51,51] 50)
"P \<turnstile> E \<surd> ≡ ∀V T. E V = Some T --> is_type P T"
section{* Type conformance *}
primrec
type_conf :: "prog => env => heap => expr => ty => bool"
("_,_,_ \<turnstile> _ :NT _" [51,51,51]50)
where
type_conf_Void: "P,E,h \<turnstile> e :NT Void <-> (P,E,h \<turnstile> e : Void)"
| type_conf_Boolean: "P,E,h \<turnstile> e :NT Boolean <-> (P,E,h \<turnstile> e : Boolean)"
| type_conf_Integer: "P,E,h \<turnstile> e :NT Integer <-> (P,E,h \<turnstile> e : Integer)"
| type_conf_NT: "P,E,h \<turnstile> e :NT NT <-> (P,E,h \<turnstile> e : NT)"
| type_conf_Class: "P,E,h \<turnstile> e :NT Class C <->
(P,E,h \<turnstile> e : Class C ∨ P,E,h \<turnstile> e : NT)"
fun
types_conf :: "prog => env => heap => expr list => ty list => bool"
("_,_,_ \<turnstile> _ [:]NT _" [51,51,51]50)
where
"P,E,h \<turnstile> [] [:]NT [] <-> True"
| "P,E,h \<turnstile> (e#es) [:]NT (T#Ts) <->
(P,E,h \<turnstile> e:NT T ∧ P,E,h \<turnstile> es [:]NT Ts)"
| "P,E,h \<turnstile> es [:]NT Ts <-> False"
lemma wt_same_type_typeconf:
"P,E,h \<turnstile> e : T ==> P,E,h \<turnstile> e :NT T"
by(cases T) auto
lemma wts_same_types_typesconf:
"P,E,h \<turnstile> es [:] Ts ==> types_conf P E h es Ts"
proof(induct Ts arbitrary: es)
case Nil thus ?case by (auto elim:WTrts.cases)
next
case (Cons T' Ts')
have wtes:"P,E,h \<turnstile> es [:] T'#Ts'"
and IH:"!!es. P,E,h \<turnstile> es [:] Ts' ==> types_conf P E h es Ts'" by fact+
from wtes obtain e' es' where es:"es = e'#es'" by(cases es) auto
with wtes have wte':"P,E,h \<turnstile> e' : T'" and wtes':"P,E,h \<turnstile> es' [:] Ts'"
by simp_all
from IH[OF wtes'] wte' es show ?case by (fastsimp intro:wt_same_type_typeconf)
qed
lemma types_conf_smaller_types:
"!!es Ts. [|length es = length Ts'; types_conf P E h es Ts'; P \<turnstile> Ts' [≤] Ts |]
==> ∃Ts''. P,E,h \<turnstile> es [:] Ts'' ∧ P \<turnstile> Ts'' [≤] Ts"
proof(induct Ts')
case Nil thus ?case by simp
next
case (Cons S Ss)
have length:"length es = length(S#Ss)"
and types_conf:"types_conf P E h es (S#Ss)"
and subs:"P \<turnstile> (S#Ss) [≤] Ts"
and IH:"!!es Ts. [|length es = length Ss; types_conf P E h es Ss; P \<turnstile> Ss [≤] Ts|]
==> ∃Ts''. P,E,h \<turnstile> es [:] Ts'' ∧ P \<turnstile> Ts'' [≤] Ts" by fact+
from subs obtain U Us where Ts:"Ts = U#Us" by(cases Ts) auto
from length obtain e' es' where es:"es = e'#es'" by(cases es) auto
with types_conf have type:"P,E,h \<turnstile> e' :NT S"
and type':"types_conf P E h es' Ss" by simp_all
from subs Ts have subs':"P \<turnstile> Ss [≤] Us" and sub:"P \<turnstile> S ≤ U"
by (simp_all add:fun_of_def)
from sub type obtain T'' where step:"P,E,h \<turnstile> e' : T'' ∧ P \<turnstile> T'' ≤ U"
by(cases S,auto,cases U,auto)
from length es have "length es' = length Ss" by simp
from IH[OF this type' subs'] obtain Ts''
where "P,E,h \<turnstile> es' [:] Ts'' ∧ P \<turnstile> Ts'' [≤] Us"
by auto
with step have "P,E,h \<turnstile> (e'#es') [:] (T''#Ts'') ∧ P \<turnstile> (T''#Ts'') [≤] (U#Us)"
by (auto simp:fun_of_def)
with es Ts show ?case by blast
qed
end