Theory Conform

(*  Title:      HOL/MicroJava/J/Conform.thy
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

section ‹Conformity Relations for Type Soundness Proof›

theory Conform imports State WellType Exceptions begin

type_synonym 'c env' = "'c prog × (vname ⇀ ty)"  ― ‹same as ‹env› of ‹WellType.thy››

definition hext :: "aheap => aheap => bool" ("_ ≤| _" [51,51] 50) where
 "h≤|h' == ∀a C fs. h a = Some(C,fs) --> (∃fs'. h' a = Some(C,fs'))"

definition conf :: "'c prog => aheap => val => ty => bool" 
                                   ("_,_ ⊢ _ ::≼ _"  [51,51,51,51] 50) where
 "G,h⊢v::≼T == ∃T'. typeof (map_option obj_ty o h) v = Some T' ∧ G⊢T'≼T"

definition lconf :: "'c prog => aheap => ('a ⇀ val) => ('a ⇀ ty) => bool"
                                   ("_,_ ⊢ _ [::≼] _" [51,51,51,51] 50) where
 "G,h⊢vs[::≼]Ts == ∀n T. Ts n = Some T --> (∃v. vs n = Some v ∧ G,h⊢v::≼T)"

definition oconf :: "'c prog => aheap => obj => bool" ("_,_ ⊢ _ √" [51,51,51] 50) where
 "G,h⊢obj √ == G,h⊢snd obj[::≼]map_of (fields (G,fst obj))"

definition hconf :: "'c prog => aheap => bool" ("_ ⊢h _ √" [51,51] 50) where
 "G⊢h h √    == ∀a obj. h a = Some obj --> G,h⊢obj √"
 
definition xconf :: "aheap ⇒ val option ⇒ bool" where
  "xconf hp vo  == preallocated hp ∧ (∀ v. (vo = Some v) ⟶ (∃ xc. v = (Addr (XcptRef xc))))"

definition conforms :: "xstate => java_mb env' => bool" ("_ ::≼ _" [51,51] 50) where
 "s::≼E == prg E⊢h heap (store s) √ ∧ 
            prg E,heap (store s)⊢locals (store s)[::≼]localT E ∧ 
            xconf (heap (store s)) (abrupt s)"


subsection "hext"

lemma hextI: 
" ∀a C fs . h  a = Some (C,fs) -->   
      (∃fs'. h' a = Some (C,fs')) ==> h≤|h'"
apply (unfold hext_def)
apply auto
done

lemma hext_objD: "[|h≤|h'; h a = Some (C,fs) |] ==> ∃fs'. h' a = Some (C,fs')"
apply (unfold hext_def)
apply (force)
done

lemma hext_refl [simp]: "h≤|h"
apply (rule hextI)
apply (fast)
done

lemma hext_new [simp]: "h a = None ==> h≤|h(a↦x)"
apply (rule hextI)
apply auto
done

lemma hext_trans: "[|h≤|h'; h'≤|h''|] ==> h≤|h''"
apply (rule hextI)
apply (fast dest: hext_objD)
done

lemma hext_upd_obj: "h a = Some (C,fs) ==> h≤|h(a↦(C,fs'))"
apply (rule hextI)
apply auto
done


subsection "conf"

lemma conf_Null [simp]: "G,h⊢Null::≼T = G⊢RefT NullT≼T"
apply (unfold conf_def)
apply (simp (no_asm))
done

lemma conf_litval [rule_format (no_asm), simp]: 
  "typeof (λv. None) v = Some T --> G,h⊢v::≼T"
apply (unfold conf_def)
apply (rule val.induct)
apply auto
done

lemma conf_AddrI: "[|h a = Some obj; G⊢obj_ty obj≼T|] ==> G,h⊢Addr a::≼T"
apply (unfold conf_def)
apply (simp)
done

lemma conf_obj_AddrI: "[|h a = Some (C,fs); G⊢C≼C D|] ==> G,h⊢Addr a::≼ Class D"
apply (unfold conf_def)
apply (simp)
done

lemma defval_conf [rule_format (no_asm)]: 
  "is_type G T --> G,h⊢default_val T::≼T"
apply (unfold conf_def)
apply (rule_tac y = "T" in ty.exhaust)
apply  (erule ssubst)
apply  (rename_tac prim_ty, rule_tac y = "prim_ty" in prim_ty.exhaust)
apply    (auto simp add: widen.null)
done

lemma conf_upd_obj: 
"h a = Some (C,fs) ==> (G,h(a↦(C,fs'))⊢x::≼T) = (G,h⊢x::≼T)"
apply (unfold conf_def)
apply (rule val.induct)
apply auto
done

lemma conf_widen [rule_format (no_asm)]: 
  "wf_prog wf_mb G ==> G,h⊢x::≼T --> G⊢T≼T' --> G,h⊢x::≼T'"
apply (unfold conf_def)
apply (rule val.induct)
apply (auto intro: widen_trans)
done

lemma conf_hext [rule_format (no_asm)]: "h≤|h' ==> G,h⊢v::≼T --> G,h'⊢v::≼T"
apply (unfold conf_def)
apply (rule val.induct)
apply (auto dest: hext_objD)
done

lemma new_locD: "[|h a = None; G,h⊢Addr t::≼T|] ==> t≠a"
apply (unfold conf_def)
apply auto
done

lemma conf_RefTD [rule_format]: 
 "G,h⊢a'::≼RefT T ⟹ a' = Null ∨
  (∃a obj T'. a' = Addr a ∧  h a = Some obj ∧  obj_ty obj = T' ∧  G⊢T'≼RefT T)"
unfolding conf_def by (induct a') auto

lemma conf_NullTD: "G,h⊢a'::≼RefT NullT ==> a' = Null"
apply (drule conf_RefTD)
apply auto
done

lemma non_npD: "[|a' ≠ Null; G,h⊢a'::≼RefT t|] ==>  
  ∃a C fs. a' = Addr a ∧  h a = Some (C,fs) ∧  G⊢Class C≼RefT t"
apply (drule conf_RefTD)
apply auto
done

lemma non_np_objD: "!!G. [|a' ≠ Null; G,h⊢a'::≼ Class C|] ==>  
  (∃a C' fs. a' = Addr a ∧  h a = Some (C',fs) ∧  G⊢C'≼C C)"
apply (fast dest: non_npD)
done

lemma non_np_objD' [rule_format (no_asm)]: 
  "a' ≠ Null ==> wf_prog wf_mb G ==> G,h⊢a'::≼RefT t --> 
  (∃a C fs. a' = Addr a ∧  h a = Some (C,fs) ∧  G⊢Class C≼RefT t)"
apply(rule_tac y = "t" in ref_ty.exhaust)
 apply (fast dest: conf_NullTD)
apply (fast dest: non_np_objD)
done

lemma conf_list_gext_widen [rule_format (no_asm)]: 
  "wf_prog wf_mb G ==> ∀Ts Ts'. list_all2 (conf G h) vs Ts --> 
  list_all2 (λT T'. G⊢T≼T') Ts Ts' -->  list_all2 (conf G h) vs Ts'"
apply(induct_tac "vs")
 apply(clarsimp)
apply(clarsimp)
apply(frule list_all2_lengthD [symmetric])
apply(simp (no_asm_use) add: length_Suc_conv)
apply(safe)
apply(frule list_all2_lengthD [symmetric])
apply(simp (no_asm_use) add: length_Suc_conv)
apply(clarify)
apply(fast elim: conf_widen)
done


subsection "lconf"

lemma lconfD: "[| G,h⊢vs[::≼]Ts; Ts n = Some T |] ==> G,h⊢(the (vs n))::≼T"
apply (unfold lconf_def)
apply (force)
done

lemma lconf_hext [elim]: "[| G,h⊢l[::≼]L; h≤|h' |] ==> G,h'⊢l[::≼]L"
apply (unfold lconf_def)
apply  (fast elim: conf_hext)
done

lemma lconf_upd: "!!X. [| G,h⊢l[::≼]lT;  
  G,h⊢v::≼T; lT va = Some T |] ==> G,h⊢l(va↦v)[::≼]lT"
apply (unfold lconf_def)
apply auto
done

lemma lconf_init_vars_lemma [rule_format (no_asm)]: 
  "∀x. P x --> R (dv x) x ==> (∀x. map_of fs f = Some x --> P x) -->  
  (∀T. map_of fs f = Some T -->  
  (∃v. map_of (map (λ(f,ft). (f, dv ft)) fs) f = Some v ∧  R v T))"
apply( induct_tac "fs")
apply auto
done

lemma lconf_init_vars [intro!]: 
"∀n. ∀T. map_of fs n = Some T --> is_type G T ==> G,h⊢init_vars fs[::≼]map_of fs"
apply (unfold lconf_def init_vars_def)
apply auto
apply( rule lconf_init_vars_lemma)
apply(   erule_tac [3] asm_rl)
apply(  intro strip)
apply(  erule defval_conf)
apply auto
done

lemma lconf_ext: "[|G,s⊢l[::≼]L; G,s⊢v::≼T|] ==> G,s⊢l(vn↦v)[::≼]L(vn↦T)"
apply (unfold lconf_def)
apply auto
done

lemma lconf_ext_list [rule_format (no_asm)]: 
  "G,h⊢l[::≼]L ==> ∀vs Ts. distinct vns --> length Ts = length vns --> 
  list_all2 (λv T. G,h⊢v::≼T) vs Ts --> G,h⊢l(vns[↦]vs)[::≼]L(vns[↦]Ts)"
apply (unfold lconf_def)
apply( induct_tac "vns")
apply(  clarsimp)
apply( clarsimp)
apply( frule list_all2_lengthD)
apply( auto simp add: length_Suc_conv)
done

lemma lconf_restr: "⟦lT vn = None; G, h ⊢ l [::≼] lT(vn↦T)⟧ ⟹ G, h ⊢ l [::≼] lT"
apply (unfold lconf_def)
apply (intro strip)
apply (case_tac "n = vn")
apply auto
done

subsection "oconf"

lemma oconf_hext: "G,h⊢obj√ ==> h≤|h' ==> G,h'⊢obj√"
apply (unfold oconf_def)
apply (fast)
done

lemma oconf_obj: "G,h⊢(C,fs)√ =  
  (∀T f. map_of(fields (G,C)) f = Some T --> (∃v. fs f = Some v ∧  G,h⊢v::≼T))"
apply (unfold oconf_def lconf_def)
apply auto
done

lemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp]


subsection "hconf"

lemma hconfD: "[|G⊢h h√; h a = Some obj|] ==> G,h⊢obj√"
apply (unfold hconf_def)
apply (fast)
done

lemma hconfI: "∀a obj. h a=Some obj --> G,h⊢obj√ ==> G⊢h h√"
apply (unfold hconf_def)
apply (fast)
done


subsection "xconf"

lemma xconf_raise_if: "xconf h x ⟹ xconf h (raise_if b xcn x)"
by (simp add: xconf_def raise_if_def)



subsection "conforms"

lemma conforms_heapD: "(x, (h, l))::≼(G, lT) ==> G⊢h h√"
apply (unfold conforms_def)
apply (simp)
done

lemma conforms_localD: "(x, (h, l))::≼(G, lT) ==> G,h⊢l[::≼]lT"
apply (unfold conforms_def)
apply (simp)
done

lemma conforms_xcptD: "(x, (h, l))::≼(G, lT) ==> xconf h x"
apply (unfold conforms_def)
apply (simp)
done

lemma conformsI: "[|G⊢h h√; G,h⊢l[::≼]lT; xconf h x|] ==> (x, (h, l))::≼(G, lT)"
apply (unfold conforms_def)
apply auto
done

lemma conforms_restr: "⟦lT vn = None; s ::≼ (G, lT(vn↦T)) ⟧ ⟹ s ::≼ (G, lT)"
by (simp add: conforms_def, fast intro: lconf_restr)

lemma conforms_xcpt_change: "⟦ (x, (h,l))::≼ (G, lT); xconf h x ⟶ xconf h x' ⟧ ⟹ (x', (h,l))::≼ (G, lT)"
by (simp add: conforms_def)


lemma preallocated_hext: "⟦ preallocated h; h≤|h'⟧ ⟹ preallocated h'"
by (simp add: preallocated_def hext_def)

lemma xconf_hext: "⟦ xconf h vo; h≤|h'⟧ ⟹ xconf h' vo"
by (simp add: xconf_def preallocated_def hext_def)

lemma conforms_hext: "[|(x,(h,l))::≼(G,lT); h≤|h'; G⊢h h'√ |] 
  ==> (x,(h',l))::≼(G,lT)"
by (fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)


lemma conforms_upd_obj: 
  "[|(x,(h,l))::≼(G, lT); G,h(a↦obj)⊢obj√; h≤|h(a↦obj)|] 
  ==> (x,(h(a↦obj),l))::≼(G, lT)"
apply(rule conforms_hext)
apply  auto
apply(rule hconfI)
apply(drule conforms_heapD)
apply(auto elim: oconf_hext dest: hconfD)
done

lemma conforms_upd_local: 
"[|(x,(h, l))::≼(G, lT); G,h⊢v::≼T; lT va = Some T|] 
  ==> (x,(h, l(va↦v)))::≼(G, lT)"
apply (unfold conforms_def)
apply( auto elim: lconf_upd)
done

end