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 (simp add:map_of_map)
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"
by(simp add:lconf_def)

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


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" 
    by (simp_all add:fun_of_def)
  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