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  typeofh v = Some Void)"
| "P,h  v :≤ Boolean   = (P  typeofh v = Some Boolean)"
| "P,h  v :≤ Integer   = (P  typeofh v = Some Integer)"
| "P,h  v :≤ NT        = (P  typeofh v = Some NT)"
| "P,h  v :≤ (Class C) = (P  typeofh v = Some(Class C)  P  typeofh v = Some NT)"

definition fconf :: "prog  heap  ('a  val)  ('a  ty)  bool" ("_,_  _ '(:≤') _" [51,51,51,51] 50) where
  "P,h  vm (:≤) Tm  
  FD T. Tm FD = Some T  (v. vm 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  vm (:≤)w Tm  
  V v. vm V = Some v  (T. Tm 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  typeofh 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  typeofh v = Some T) = (P  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(C,S'))  v :≤ T) = (P,h  v :≤ T)"

proof(cases T)
  case Void
  hence "(P  typeofh(a(C,S')) v = Some T) = (P  typeofh v = Some T)"
    by(fastforce intro!:typeof_notclass_heap)
  with Void show ?thesis by simp
next
  case Boolean
  hence "(P  typeofh(a(C,S')) v = Some T) = (P  typeofh v = Some T)"
    by(fastforce intro!:typeof_notclass_heap)
  with Boolean show ?thesis by simp
next
  case Integer
  hence "(P  typeofh(a(C,S')) v = Some T) = (P  typeofh v = Some T)"
    by(fastforce intro!:typeof_notclass_heap)
  with Integer show ?thesis by simp
next
  case NT
  hence "(P  typeofh(a(C,S')) v = Some T) = (P  typeofh v = Some T)"
    by(fastforce intro!:typeof_notclass_heap)
  with NT show ?thesis by simp
next
  case (Class C')
  { assume "P  typeofh(a  (C, S')) v = Some(Class C')"
    with h have "P  typeofh v = Some(Class C')"
      by (cases v) (auto split:if_split_asm)  }
  hence 1:"P  typeofh(a  (C, S')) v = Some(Class C')  
           P  typeofh v = Some(Class C')" by simp
  { assume type:"P  typeofh(a  (C, S')) v = Some NT"
    and typenot:"P  typeofh v  Some NT"
    have "C. NT  Class C" by simp
    with type have "P  typeofh v = Some NT" by(fastforce dest:typeof_notclass_heap)
    with typenot have "P  typeofh v = Some(Class C')" by simp }
  hence 2:"P  typeofh(a  (C, S')) v = Some NT; P  typeofh v  Some NT 
    P  typeofh v = Some(Class C')" by simp
  { assume "P  typeofh v = Some(Class C')"
    with h have "P  typeofh(a  (C, S')) v = Some(Class C')"
      by (cases v) (auto split:if_split_asm) }
  hence 3:"P  typeofh v = Some(Class C')  
           P  typeofh(a  (C, S')) v = Some(Class C')" by simp
  { assume typenot:"P  typeofh(a  (C, S')) v  Some NT"
    and type:"P  typeofh v = Some NT"
    have "C. NT  Class C" by simp
    with type have "P  typeofh(a  (C, S')) v = Some NT" 
      by(fastforce dest:typeof_notclass_heap)
    with typenot have "P  typeofh(a  (C, S')) v = Some(Class C')" by simp }
  hence 4:"P  typeofh(a  (C, S')) v  Some NT; P  typeofh v = Some NT 
    P  typeofh(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(Vv) (:≤)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(Vv) (:≤)w E(VT)"
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