# Theory Conform

Up to index of Isabelle/HOL/HOL-MicroJava-skip_proofs

theory Conform
imports WellType Exceptions
`(*  Title:      HOL/MicroJava/J/Conform.thy    Author:     David von Oheimb    Copyright   1999 Technische Universitaet Muenchen*)header {* \isaheader{Conformity Relations for Type Soundness Proof} *}theory Conform imports State WellType Exceptions begintype_synonym 'c env' = "'c prog × (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text 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 (Option.map obj_ty o h) v = Some T' ∧ G\<turnstile>T'\<preceq>T"definition lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> 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" ("_,_ |- _ [ok]" [51,51,51] 50) where "G,h|-obj [ok] == G,h|-snd obj[::<=]map_of (fields (G,fst obj))"definition hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50) where "G|-h h [ok]    == ∀a obj. h a = Some obj --> G,h|-obj [ok]" 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) [ok] ∧             prg E,heap (store s)|-locals (store s)[::<=]localT E ∧             xconf (heap (store s)) (abrupt s)"notation (xsymbols)  hext  ("_ ≤| _" [51,51] 50) and  conf  ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and  lconf  ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and  oconf  ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and  hconf  ("_ \<turnstile>h _ \<surd>" [51,51] 50) and  conforms  ("_ ::\<preceq> _" [51,51] 50)section "hext"lemma hextI: " ∀a C fs . h  a = Some (C,fs) -->         (∃fs'. h' a = Some (C,fs')) ==> h≤|h'"apply (unfold hext_def)apply autodonelemma hext_objD: "[|h≤|h'; h a = Some (C,fs) |] ==> ∃fs'. h' a = Some (C,fs')"apply (unfold hext_def)apply (force)donelemma hext_refl [simp]: "h≤|h"apply (rule hextI)apply (fast)donelemma hext_new [simp]: "h a = None ==> h≤|h(a\<mapsto>x)"apply (rule hextI)apply autodonelemma hext_trans: "[|h≤|h'; h'≤|h''|] ==> h≤|h''"apply (rule hextI)apply (fast dest: hext_objD)donelemma hext_upd_obj: "h a = Some (C,fs) ==> h≤|h(a\<mapsto>(C,fs'))"apply (rule hextI)apply autodonesection "conf"lemma conf_Null [simp]: "G,h\<turnstile>Null::\<preceq>T = G\<turnstile>RefT NullT\<preceq>T"apply (unfold conf_def)apply (simp (no_asm))donelemma conf_litval [rule_format (no_asm), simp]:   "typeof (λv. None) v = Some T --> G,h\<turnstile>v::\<preceq>T"apply (unfold conf_def)apply (rule val.induct)apply autodonelemma conf_AddrI: "[|h a = Some obj; G\<turnstile>obj_ty obj\<preceq>T|] ==> G,h\<turnstile>Addr a::\<preceq>T"apply (unfold conf_def)apply (simp)donelemma conf_obj_AddrI: "[|h a = Some (C,fs); G\<turnstile>C\<preceq>C D|] ==> G,h\<turnstile>Addr a::\<preceq> Class D"apply (unfold conf_def)apply (simp)donelemma defval_conf [rule_format (no_asm)]:   "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"apply (unfold conf_def)apply (rule_tac y = "T" in ty.exhaust)apply  (erule ssubst)apply  (rule_tac y = "prim_ty" in prim_ty.exhaust)apply    (auto simp add: widen.null)donelemma conf_upd_obj: "h a = Some (C,fs) ==> (G,h(a\<mapsto>(C,fs'))\<turnstile>x::\<preceq>T) = (G,h\<turnstile>x::\<preceq>T)"apply (unfold conf_def)apply (rule val.induct)apply autodonelemma conf_widen [rule_format (no_asm)]:   "wf_prog wf_mb G ==> G,h\<turnstile>x::\<preceq>T --> G\<turnstile>T\<preceq>T' --> G,h\<turnstile>x::\<preceq>T'"apply (unfold conf_def)apply (rule val.induct)apply (auto intro: widen_trans)donelemma conf_hext [rule_format (no_asm)]: "h≤|h' ==> G,h\<turnstile>v::\<preceq>T --> G,h'\<turnstile>v::\<preceq>T"apply (unfold conf_def)apply (rule val.induct)apply (auto dest: hext_objD)donelemma new_locD: "[|h a = None; G,h\<turnstile>Addr t::\<preceq>T|] ==> t≠a"apply (unfold conf_def)apply autodonelemma conf_RefTD [rule_format (no_asm)]:  "G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null |     (∃a obj T'. a' = Addr a ∧  h a = Some obj ∧  obj_ty obj = T' ∧  G\<turnstile>T'\<preceq>RefT T)"apply (unfold conf_def)apply(induct_tac "a'")apply(auto)donelemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null"apply (drule conf_RefTD)apply autodonelemma non_npD: "[|a' ≠ Null; G,h\<turnstile>a'::\<preceq>RefT t|] ==>    ∃a C fs. a' = Addr a ∧  h a = Some (C,fs) ∧  G\<turnstile>Class C\<preceq>RefT t"apply (drule conf_RefTD)apply autodonelemma non_np_objD: "!!G. [|a' ≠ Null; G,h\<turnstile>a'::\<preceq> Class C|] ==>    (∃a C' fs. a' = Addr a ∧  h a = Some (C',fs) ∧  G\<turnstile>C'\<preceq>C C)"apply (fast dest: non_npD)donelemma non_np_objD' [rule_format (no_asm)]:   "a' ≠ Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t -->   (∃a C fs. a' = Addr a ∧  h a = Some (C,fs) ∧  G\<turnstile>Class C\<preceq>RefT t)"apply(rule_tac y = "t" in ref_ty.exhaust) apply (fast dest: conf_NullTD)apply (fast dest: non_np_objD)donelemma 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\<turnstile>T\<preceq>T') Ts Ts' -->  list_all2 (conf G h) vs Ts'"apply(induct_tac "vs") apply(clarsimp)apply(clarsimp)apply(frule list_all2_lengthD [THEN sym])apply(simp (no_asm_use) add: length_Suc_conv)apply(safe)apply(frule list_all2_lengthD [THEN sym])apply(simp (no_asm_use) add: length_Suc_conv)apply(clarify)apply(fast elim: conf_widen)donesection "lconf"lemma lconfD: "[| G,h\<turnstile>vs[::\<preceq>]Ts; Ts n = Some T |] ==> G,h\<turnstile>(the (vs n))::\<preceq>T"apply (unfold lconf_def)apply (force)donelemma lconf_hext [elim]: "[| G,h\<turnstile>l[::\<preceq>]L; h≤|h' |] ==> G,h'\<turnstile>l[::\<preceq>]L"apply (unfold lconf_def)apply  (fast elim: conf_hext)donelemma lconf_upd: "!!X. [| G,h\<turnstile>l[::\<preceq>]lT;    G,h\<turnstile>v::\<preceq>T; lT va = Some T |] ==> G,h\<turnstile>l(va\<mapsto>v)[::\<preceq>]lT"apply (unfold lconf_def)apply autodonelemma 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 autodonelemma lconf_init_vars [intro!]: "∀n. ∀T. map_of fs n = Some T --> is_type G T ==> G,h\<turnstile>init_vars fs[::\<preceq>]map_of fs"apply (unfold lconf_def init_vars_def)apply autoapply( rule lconf_init_vars_lemma)apply(   erule_tac [3] asm_rl)apply(  intro strip)apply(  erule defval_conf)apply autodonelemma lconf_ext: "[|G,s\<turnstile>l[::\<preceq>]L; G,s\<turnstile>v::\<preceq>T|] ==> G,s\<turnstile>l(vn\<mapsto>v)[::\<preceq>]L(vn\<mapsto>T)"apply (unfold lconf_def)apply autodonelemma lconf_ext_list [rule_format (no_asm)]:   "G,h\<turnstile>l[::\<preceq>]L ==> ∀vs Ts. distinct vns --> length Ts = length vns -->   list_all2 (λv T. G,h\<turnstile>v::\<preceq>T) vs Ts --> G,h\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]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)donelemma lconf_restr: "[|lT vn = None; G, h \<turnstile> l [::\<preceq>] lT(vn\<mapsto>T)|] ==> G, h \<turnstile> l [::\<preceq>] lT"apply (unfold lconf_def)apply (intro strip)apply (case_tac "n = vn")apply autodonesection "oconf"lemma oconf_hext: "G,h\<turnstile>obj\<surd> ==> h≤|h' ==> G,h'\<turnstile>obj\<surd>"apply (unfold oconf_def)apply (fast)donelemma oconf_obj: "G,h\<turnstile>(C,fs)\<surd> =    (∀T f. map_of(fields (G,C)) f = Some T --> (∃v. fs f = Some v ∧  G,h\<turnstile>v::\<preceq>T))"apply (unfold oconf_def lconf_def)apply autodonelemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp]section "hconf"lemma hconfD: "[|G\<turnstile>h h\<surd>; h a = Some obj|] ==> G,h\<turnstile>obj\<surd>"apply (unfold hconf_def)apply (fast)donelemma hconfI: "∀a obj. h a=Some obj --> G,h\<turnstile>obj\<surd> ==> G\<turnstile>h h\<surd>"apply (unfold hconf_def)apply (fast)donesection "xconf"lemma xconf_raise_if: "xconf h x ==> xconf h (raise_if b xcn x)"by (simp add: xconf_def raise_if_def)section "conforms"lemma conforms_heapD: "(x, (h, l))::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"apply (unfold conforms_def)apply (simp)donelemma conforms_localD: "(x, (h, l))::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT"apply (unfold conforms_def)apply (simp)donelemma conforms_xcptD: "(x, (h, l))::\<preceq>(G, lT) ==> xconf h x"apply (unfold conforms_def)apply (simp)donelemma conformsI: "[|G\<turnstile>h h\<surd>; G,h\<turnstile>l[::\<preceq>]lT; xconf h x|] ==> (x, (h, l))::\<preceq>(G, lT)"apply (unfold conforms_def)apply autodonelemma conforms_restr: "[|lT vn = None; s ::\<preceq> (G, lT(vn\<mapsto>T)) |] ==> s ::\<preceq> (G, lT)"by (simp add: conforms_def, fast intro: lconf_restr)lemma conforms_xcpt_change: "[| (x, (h,l))::\<preceq> (G, lT); xconf h x --> xconf h x' |] ==> (x', (h,l))::\<preceq> (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))::\<preceq>(G,lT); h≤|h'; G\<turnstile>h h'\<surd> |]   ==> (x,(h',l))::\<preceq>(G,lT)"by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)lemma conforms_upd_obj:   "[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h≤|h(a\<mapsto>obj)|]   ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)"apply(rule conforms_hext)apply  autoapply(rule hconfI)apply(drule conforms_heapD)apply(auto elim: oconf_hext dest: hconfD)donelemma conforms_upd_local: "[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|]   ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)"apply (unfold conforms_def)apply( auto elim: lconf_upd)doneend`