Theory Conform

(*  Title:      Jinja/J/Conform.thy
    ID:         $Id: Conform.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     David von Oheimb, Tobias Nipkow
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Conformance Relations for Type Soundness Proofs} *}

theory Conform = Exceptions:

constdefs
  conf :: "'m prog => heap => val => ty => bool"   ("_,_ \<turnstile> _ :≤ _"  [51,51,51,51] 50)
  "P,h \<turnstile> v :≤ T  ≡
  ∃T'. typeofh v = Some T' ∧ P \<turnstile> T' ≤ T"

  fconf :: "'m prog => heap => ('a => val) => ('a => 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 :: "'m prog => heap => obj => bool"   ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50)
  "P,h \<turnstile> obj \<surd>  ≡
  let (C,vm) = obj in ∃FDTs. P \<turnstile> C has_fields FDTs ∧ P,h \<turnstile> vm (:≤) map_of FDTs"

  hconf :: "'m 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 :: "'m prog => heap => ('a => val) => ('a => 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)"

(*<*)
syntax
  confs :: "'m prog => heap => val list => ty list => bool" 
           ("_,_ \<turnstile> _ [:≤] _" [51,51,51,51] 50)
(*>*)

translations
  "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]: "is_type P T ==> P,h \<turnstile> default_val T :≤ T"
(*<*)
apply (unfold conf_def)
apply (cases T)
apply auto
done
(*>*)

lemma conf_upd_obj: "h a = Some(C,fs) ==> (P,h(a\<mapsto>(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_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"
(*<*)
apply (unfold conf_def)
apply (induct v)
apply (auto dest: hext_objD)
done
(*>*)

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)
done
(*>*)

lemma conf_NT [iff]: "P,h \<turnstile> v :≤ NT = (v = Null)"
(*<*)by (auto simp add: conf_def)(*>*)
(*
lemma non_npD: "[| v ≠ Null; P,h \<turnstile> v :≤ Class C |]
  ==> ∃a D fs. v = Addr a ∧ h a = Some(D,fs) ∧ P \<turnstile> Class D ≤ Class C"
apply (drule conf_ClassD)
apply auto
done
*)

lemma non_npD: "[| v ≠ Null; P,h \<turnstile> v :≤ Class C |]
  ==> ∃a C' fs. v = Addr a ∧ h a = Some(C',fs) ∧ P \<turnstile> C' \<preceq>* C"
(*<*)
apply (drule conf_ClassD)
apply auto
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)
    apply (rule conf_widen, assumption, assumption)
   apply assumption
  apply (fold fun_of_def, assumption)
  done
(*>*)

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)
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{* Field conformance @{text"(:≤)"} *}

lemma fconf_hext: "[| P,h \<turnstile> fvs (:≤) E; h \<unlhd> h' |] ==> P,h' \<turnstile> fvs (:≤) E"
(*<*)
apply (unfold fconf_def)
apply  (fast elim: conf_hext)
done
(*>*)

lemma fconf_init_fields: "P,h \<turnstile> init_fields fs (:≤) map_of fs"
(*<*)
apply(unfold fconf_def init_fields_def)
apply(induct fs)
apply (auto simp:fun_upd_apply)
apply(rename_tac T list)
apply(case_tac T)
apply simp_all
done
(*>*)


section "Object conformance"

lemma oconf_hext: "P,h \<turnstile> obj \<surd> ==> h \<unlhd> h' ==> P,h' \<turnstile> obj \<surd>"
(*<*)
apply (unfold oconf_def)
apply (auto elim:fconf_hext)
done
(*>*)

lemma oconf_fupd [intro?]:
  "[| P \<turnstile> C has F:T in D; P,h \<turnstile> v :≤ T; P,h \<turnstile> (C,fs) \<surd> |] 
  ==> P,h \<turnstile> (C, fs((F,D)\<mapsto>v)) \<surd>"
(*<*)
  apply (unfold oconf_def fconf_def has_field_def)
  apply clarsimp
  apply (drule (1) has_fields_fun)
  apply (auto simp add: fun_upd_apply)
  done                                    
(*>*)

(*<*)
lemmas oconf_new = oconf_hext [OF _ hext_new]
lemmas oconf_upd_obj = oconf_hext [OF _ hext_upd_obj]
(*>*)

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(C,fs); P,h \<turnstile> (C,fs')\<surd> |] ==> P \<turnstile> h(a\<mapsto>(C,fs'))\<surd>"
(*<*)by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)(*>*)


section "Local variable conformance"

lemma lconf_hext: "[| P,h \<turnstile> l (:≤)w E; h \<unlhd> h' |] ==> P,h' \<turnstile> l (:≤)w E"
(*<*)
apply (unfold lconf_def)
apply  (fast elim: conf_hext)
done
(*>*)

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)(*>*)


end