# Theory Conform

```(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on the Jinja theory Common/Conform.thy by David von Oheimb and Tobias Nipkow
*)

section ‹Conformance Relations for Proofs›

theory Conform
imports Exceptions WellTypeRT
begin

primrec conf :: "prog ⇒ heap ⇒ val ⇒ ty ⇒ bool"   ("_,_ ⊢ _ :≤ _"  [51,51,51,51] 50) where
"P,h ⊢ v :≤ Void      = (P ⊢ typeof⇘h⇙ v = Some Void)"
| "P,h ⊢ v :≤ Boolean   = (P ⊢ typeof⇘h⇙ v = Some Boolean)"
| "P,h ⊢ v :≤ Integer   = (P ⊢ typeof⇘h⇙ v = Some Integer)"
| "P,h ⊢ v :≤ NT        = (P ⊢ typeof⇘h⇙ v = Some NT)"
| "P,h ⊢ v :≤ (Class C) = (P ⊢ typeof⇘h⇙ v = Some(Class C) ∨ P ⊢ typeof⇘h⇙ v = Some NT)"

definition fconf :: "prog ⇒ heap ⇒ ('a ⇀ val) ⇒ ('a ⇀ ty) ⇒ bool" ("_,_ ⊢ _ '(:≤') _" [51,51,51,51] 50) where
"P,h ⊢ v⇩m (:≤) T⇩m  ≡
∀FD T. T⇩m FD = Some T ⟶ (∃v. v⇩m FD = Some v ∧ P,h ⊢ v :≤ T)"

definition oconf :: "prog ⇒ heap ⇒ obj ⇒ bool"   ("_,_ ⊢ _ √" [51,51,51] 50) where
"P,h ⊢ obj √  ≡ 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 ⊢ fs' (:≤) map_of fs))"

definition hconf :: "prog ⇒ heap ⇒ bool"  ("_ ⊢ _ √" [51,51] 50) where
"P ⊢ h √  ≡
(∀a obj. h a = Some obj ⟶ P,h ⊢ obj √) ∧ preallocated h"

definition lconf :: "prog ⇒ heap ⇒ ('a ⇀ val) ⇒ ('a ⇀ ty) ⇒ bool"   ("_,_ ⊢ _ '(:≤')⇩w _" [51,51,51,51] 50) where
"P,h ⊢ v⇩m (:≤)⇩w T⇩m  ≡
∀V v. v⇩m V = Some v ⟶ (∃T. T⇩m V = Some T ∧ P,h ⊢ v :≤ T)"

abbreviation
confs :: "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(cases T) simp_all

lemma typeof_conf[simp]: "P ⊢ typeof⇘h⇙ v = Some T ⟹ P,h ⊢ v :≤ T"
by (cases T) auto

lemma typeof_lit_conf[simp]: "typeof v = Some T ⟹ P,h ⊢ v :≤ T"
by (rule typeof_conf[OF type_eq_type])

lemma defval_conf[simp]: "is_type P T ⟹ P,h ⊢ default_val T :≤ T"
by(cases T) auto

lemma typeof_notclass_heap:
"∀C. T ≠ Class C ⟹ (P ⊢ typeof⇘h⇙ v = Some T) = (P ⊢ typeof⇘h'⇙ 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↦(C,S')) ⊢ v :≤ T) = (P,h ⊢ v :≤ T)"

proof(cases T)
case Void
hence "(P ⊢ typeof⇘h(a↦(C,S'))⇙ v = Some T) = (P ⊢ typeof⇘h⇙ v = Some T)"
by(fastforce intro!:typeof_notclass_heap)
with Void show ?thesis by simp
next
case Boolean
hence "(P ⊢ typeof⇘h(a↦(C,S'))⇙ v = Some T) = (P ⊢ typeof⇘h⇙ v = Some T)"
by(fastforce intro!:typeof_notclass_heap)
with Boolean show ?thesis by simp
next
case Integer
hence "(P ⊢ typeof⇘h(a↦(C,S'))⇙ v = Some T) = (P ⊢ typeof⇘h⇙ v = Some T)"
by(fastforce intro!:typeof_notclass_heap)
with Integer show ?thesis by simp
next
case NT
hence "(P ⊢ typeof⇘h(a↦(C,S'))⇙ v = Some T) = (P ⊢ typeof⇘h⇙ v = Some T)"
by(fastforce intro!:typeof_notclass_heap)
with NT show ?thesis by simp
next
case (Class C')
{ assume "P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v = Some(Class C')"
with h have "P ⊢ typeof⇘h⇙ v = Some(Class C')"
by (cases v) (auto split:if_split_asm)  }
hence 1:"P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v = Some(Class C') ⟹
P ⊢ typeof⇘h⇙ v = Some(Class C')" by simp
{ assume type:"P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v = Some NT"
and typenot:"P ⊢ typeof⇘h⇙ v ≠ Some NT"
have "∀C. NT ≠ Class C" by simp
with type have "P ⊢ typeof⇘h⇙ v = Some NT" by(fastforce dest:typeof_notclass_heap)
with typenot have "P ⊢ typeof⇘h⇙ v = Some(Class C')" by simp }
hence 2:"⟦P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v = Some NT; P ⊢ typeof⇘h⇙ v ≠ Some NT⟧ ⟹
P ⊢ typeof⇘h⇙ v = Some(Class C')" by simp
{ assume "P ⊢ typeof⇘h⇙ v = Some(Class C')"
with h have "P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v = Some(Class C')"
by (cases v) (auto split:if_split_asm) }
hence 3:"P ⊢ typeof⇘h⇙ v = Some(Class C') ⟹
P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v = Some(Class C')" by simp
{ assume typenot:"P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v ≠ Some NT"
and type:"P ⊢ typeof⇘h⇙ v = Some NT"
have "∀C. NT ≠ Class C" by simp
with type have "P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v = Some NT"
by(fastforce dest:typeof_notclass_heap)
with typenot have "P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v = Some(Class C')" by simp }
hence 4:"⟦P ⊢ typeof⇘h(a ↦ (C, S'))⇙ v ≠ Some NT; P ⊢ typeof⇘h⇙ v = Some NT⟧ ⟹
P ⊢ typeof⇘h(a ↦ (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 ⊢ v :≤ NT = (v = Null)"
by fastforce

subsection‹Value list conformance ‹[:≤]››

lemma confs_rev: "P,h ⊢ rev s [:≤] t = (P,h ⊢ 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 ⊢ xs [:≤] y#ys = (∃z zs. xs = z#zs ∧ P,h ⊢ z :≤ y ∧ P,h ⊢ zs [:≤] ys)"
by (rule list_all2_Cons2)

subsection‹Field conformance ‹(:≤)››

lemma fconf_init_fields:
"class P C = Some(Bs,fs,ms) ⟹ P,h ⊢ 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(case_tac T)
apply simp_all
done

subsection‹Heap conformance›

lemma hconfD: "⟦ P ⊢ h √; h a = Some obj ⟧ ⟹ P,h ⊢ obj √"

apply (unfold hconf_def)
apply (fast)
done

lemma hconf_Subobjs:
"⟦h a = Some(C,S); (Cs, fs) ∈ S; P ⊢ h √⟧ ⟹ 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 fastforce
done

subsection ‹Local variable conformance›

lemma lconf_upd:
"⟦ P,h ⊢ l (:≤)⇩w E; P,h ⊢ v :≤ T; E V = Some T ⟧ ⟹ P,h ⊢ l(V↦v) (:≤)⇩w E"

apply (unfold lconf_def)
apply auto
done

lemma lconf_empty[iff]: "P,h ⊢ Map.empty (:≤)⇩w E"

lemma lconf_upd2: "⟦P,h ⊢ l (:≤)⇩w E; P,h ⊢ v :≤ T⟧ ⟹ P,h ⊢ l(V↦v) (:≤)⇩w E(V↦T)"

subsection‹Environment conformance›

definition envconf :: "prog ⇒ env ⇒ bool" ("_ ⊢ _ √" [51,51] 50) where
"P ⊢ E √ ≡ ∀V T. E V = Some T ⟶ is_type P T"

subsection‹Type conformance›

primrec
type_conf :: "prog ⇒ env ⇒ heap ⇒ expr ⇒ ty ⇒ bool"
("_,_,_ ⊢ _ :⇘NT⇙ _" [51,51,51]50)
where
type_conf_Void:      "P,E,h ⊢ e :⇘NT⇙ Void    ⟷ (P,E,h ⊢ e : Void)"
| type_conf_Boolean: "P,E,h ⊢ e :⇘NT⇙ Boolean ⟷ (P,E,h ⊢ e : Boolean)"
| type_conf_Integer: "P,E,h ⊢ e :⇘NT⇙ Integer ⟷ (P,E,h ⊢ e : Integer)"
| type_conf_NT:      "P,E,h ⊢ e :⇘NT⇙ NT      ⟷ (P,E,h ⊢ e : NT)"
| type_conf_Class:   "P,E,h ⊢ e :⇘NT⇙ Class C ⟷
(P,E,h ⊢ e : Class C ∨ P,E,h ⊢ e : NT)"

fun
types_conf :: "prog ⇒ env ⇒ heap ⇒ expr list ⇒ ty list ⇒ bool"
("_,_,_ ⊢ _ [:]⇘NT⇙ _"   [51,51,51]50)
where
"P,E,h ⊢ [] [:]⇘NT⇙ [] ⟷ True"
| "P,E,h ⊢ (e#es) [:]⇘NT⇙ (T#Ts) ⟷
(P,E,h ⊢ e:⇘NT⇙ T ∧ P,E,h ⊢ es [:]⇘NT⇙ Ts)"
| "P,E,h ⊢ es [:]⇘NT⇙ Ts ⟷ False"

lemma wt_same_type_typeconf:
"P,E,h ⊢ e : T ⟹ P,E,h ⊢ e :⇘NT⇙ T"
by(cases T) auto

lemma wts_same_types_typesconf:
"P,E,h ⊢ 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 ⊢ es [:] T'#Ts'"
and IH:"⋀es. P,E,h ⊢ 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 ⊢ e' : T'" and wtes':"P,E,h ⊢ es' [:] Ts'"
by simp_all
from IH[OF wtes'] wte' es show ?case by (fastforce 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 ⊢ Ts' [≤] Ts ⟧
⟹ ∃Ts''. P,E,h ⊢ es [:] Ts'' ∧ P ⊢ 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 ⊢ (S#Ss) [≤] Ts"
and IH:"⋀es Ts. ⟦length es = length Ss; types_conf P E h es Ss; P ⊢ Ss [≤] Ts⟧
⟹ ∃Ts''. P,E,h ⊢ es [:] Ts'' ∧ P ⊢ 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 ⊢ e' :⇘NT⇙ S"
and type':"types_conf P E h es' Ss" by simp_all
from subs Ts have subs':"P ⊢ Ss [≤] Us" and sub:"P ⊢ S ≤ U"
from sub type obtain T'' where step:"P,E,h ⊢ e' : T'' ∧ P ⊢ 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 ⊢ es' [:] Ts'' ∧ P ⊢ Ts'' [≤] Us"
by auto
with step have "P,E,h ⊢ (e'#es') [:] (T''#Ts'') ∧ P ⊢ (T''#Ts'') [≤] (U#Us)"
by (auto simp:fun_of_def)
with es Ts show ?case by blast
qed

end
```