src/HOL/MicroJava/J/Conform.thy
author haftmann
Wed May 26 16:31:44 2010 +0200 (2010-05-26)
changeset 37139 e0bd5934a2fb
parent 35417 47ee18b6ae32
child 42463 f270e3e18be5
permissions -rw-r--r--
dropped legacy theorem bindings
     1 (*  Title:      HOL/MicroJava/J/Conform.thy
     2     Author:     David von Oheimb
     3     Copyright   1999 Technische Universitaet Muenchen
     4 *)
     5 
     6 header {* \isaheader{Conformity Relations for Type Soundness Proof} *}
     7 
     8 theory Conform imports State WellType Exceptions begin
     9 
    10 types 'c env' = "'c prog \<times> (vname \<rightharpoonup> ty)"  -- "same as @{text env} of @{text WellType.thy}"
    11 
    12 definition hext :: "aheap => aheap => bool" ("_ <=| _" [51,51] 50) where
    13  "h<=|h' == \<forall>a C fs. h a = Some(C,fs) --> (\<exists>fs'. h' a = Some(C,fs'))"
    14 
    15 definition conf :: "'c prog => aheap => val => ty => bool" 
    16                                    ("_,_ |- _ ::<= _"  [51,51,51,51] 50) where
    17  "G,h|-v::<=T == \<exists>T'. typeof (Option.map obj_ty o h) v = Some T' \<and> G\<turnstile>T'\<preceq>T"
    18 
    19 definition lconf :: "'c prog => aheap => ('a \<rightharpoonup> val) => ('a \<rightharpoonup> ty) => bool"
    20                                    ("_,_ |- _ [::<=] _" [51,51,51,51] 50) where
    21  "G,h|-vs[::<=]Ts == \<forall>n T. Ts n = Some T --> (\<exists>v. vs n = Some v \<and> G,h|-v::<=T)"
    22 
    23 definition oconf :: "'c prog => aheap => obj => bool" ("_,_ |- _ [ok]" [51,51,51] 50) where
    24  "G,h|-obj [ok] == G,h|-snd obj[::<=]map_of (fields (G,fst obj))"
    25 
    26 definition hconf :: "'c prog => aheap => bool" ("_ |-h _ [ok]" [51,51] 50) where
    27  "G|-h h [ok]    == \<forall>a obj. h a = Some obj --> G,h|-obj [ok]"
    28  
    29 definition xconf :: "aheap \<Rightarrow> val option \<Rightarrow> bool" where
    30   "xconf hp vo  == preallocated hp \<and> (\<forall> v. (vo = Some v) \<longrightarrow> (\<exists> xc. v = (Addr (XcptRef xc))))"
    31 
    32 definition conforms :: "xstate => java_mb env' => bool" ("_ ::<= _" [51,51] 50) where
    33  "s::<=E == prg E|-h heap (store s) [ok] \<and> 
    34             prg E,heap (store s)|-locals (store s)[::<=]localT E \<and> 
    35             xconf (heap (store s)) (abrupt s)"
    36 
    37 
    38 notation (xsymbols)
    39   hext  ("_ \<le>| _" [51,51] 50) and
    40   conf  ("_,_ \<turnstile> _ ::\<preceq> _" [51,51,51,51] 50) and
    41   lconf  ("_,_ \<turnstile> _ [::\<preceq>] _" [51,51,51,51] 50) and
    42   oconf  ("_,_ \<turnstile> _ \<surd>" [51,51,51] 50) and
    43   hconf  ("_ \<turnstile>h _ \<surd>" [51,51] 50) and
    44   conforms  ("_ ::\<preceq> _" [51,51] 50)
    45 
    46 
    47 section "hext"
    48 
    49 lemma hextI: 
    50 " \<forall>a C fs . h  a = Some (C,fs) -->   
    51       (\<exists>fs'. h' a = Some (C,fs')) ==> h\<le>|h'"
    52 apply (unfold hext_def)
    53 apply auto
    54 done
    55 
    56 lemma hext_objD: "[|h\<le>|h'; h a = Some (C,fs) |] ==> \<exists>fs'. h' a = Some (C,fs')"
    57 apply (unfold hext_def)
    58 apply (force)
    59 done
    60 
    61 lemma hext_refl [simp]: "h\<le>|h"
    62 apply (rule hextI)
    63 apply (fast)
    64 done
    65 
    66 lemma hext_new [simp]: "h a = None ==> h\<le>|h(a\<mapsto>x)"
    67 apply (rule hextI)
    68 apply auto
    69 done
    70 
    71 lemma hext_trans: "[|h\<le>|h'; h'\<le>|h''|] ==> h\<le>|h''"
    72 apply (rule hextI)
    73 apply (fast dest: hext_objD)
    74 done
    75 
    76 lemma hext_upd_obj: "h a = Some (C,fs) ==> h\<le>|h(a\<mapsto>(C,fs'))"
    77 apply (rule hextI)
    78 apply auto
    79 done
    80 
    81 
    82 section "conf"
    83 
    84 lemma conf_Null [simp]: "G,h\<turnstile>Null::\<preceq>T = G\<turnstile>RefT NullT\<preceq>T"
    85 apply (unfold conf_def)
    86 apply (simp (no_asm))
    87 done
    88 
    89 lemma conf_litval [rule_format (no_asm), simp]: 
    90   "typeof (\<lambda>v. None) v = Some T --> G,h\<turnstile>v::\<preceq>T"
    91 apply (unfold conf_def)
    92 apply (rule val.induct)
    93 apply auto
    94 done
    95 
    96 lemma conf_AddrI: "[|h a = Some obj; G\<turnstile>obj_ty obj\<preceq>T|] ==> G,h\<turnstile>Addr a::\<preceq>T"
    97 apply (unfold conf_def)
    98 apply (simp)
    99 done
   100 
   101 lemma conf_obj_AddrI: "[|h a = Some (C,fs); G\<turnstile>C\<preceq>C D|] ==> G,h\<turnstile>Addr a::\<preceq> Class D"
   102 apply (unfold conf_def)
   103 apply (simp)
   104 done
   105 
   106 lemma defval_conf [rule_format (no_asm)]: 
   107   "is_type G T --> G,h\<turnstile>default_val T::\<preceq>T"
   108 apply (unfold conf_def)
   109 apply (rule_tac y = "T" in ty.exhaust)
   110 apply  (erule ssubst)
   111 apply  (rule_tac y = "prim_ty" in prim_ty.exhaust)
   112 apply    (auto simp add: widen.null)
   113 done
   114 
   115 lemma conf_upd_obj: 
   116 "h a = Some (C,fs) ==> (G,h(a\<mapsto>(C,fs'))\<turnstile>x::\<preceq>T) = (G,h\<turnstile>x::\<preceq>T)"
   117 apply (unfold conf_def)
   118 apply (rule val.induct)
   119 apply auto
   120 done
   121 
   122 lemma conf_widen [rule_format (no_asm)]: 
   123   "wf_prog wf_mb G ==> G,h\<turnstile>x::\<preceq>T --> G\<turnstile>T\<preceq>T' --> G,h\<turnstile>x::\<preceq>T'"
   124 apply (unfold conf_def)
   125 apply (rule val.induct)
   126 apply (auto intro: widen_trans)
   127 done
   128 
   129 lemma conf_hext [rule_format (no_asm)]: "h\<le>|h' ==> G,h\<turnstile>v::\<preceq>T --> G,h'\<turnstile>v::\<preceq>T"
   130 apply (unfold conf_def)
   131 apply (rule val.induct)
   132 apply (auto dest: hext_objD)
   133 done
   134 
   135 lemma new_locD: "[|h a = None; G,h\<turnstile>Addr t::\<preceq>T|] ==> t\<noteq>a"
   136 apply (unfold conf_def)
   137 apply auto
   138 done
   139 
   140 lemma conf_RefTD [rule_format (no_asm)]: 
   141  "G,h\<turnstile>a'::\<preceq>RefT T --> a' = Null |   
   142   (\<exists>a obj T'. a' = Addr a \<and>  h a = Some obj \<and>  obj_ty obj = T' \<and>  G\<turnstile>T'\<preceq>RefT T)"
   143 apply (unfold conf_def)
   144 apply(induct_tac "a'")
   145 apply(auto)
   146 done
   147 
   148 lemma conf_NullTD: "G,h\<turnstile>a'::\<preceq>RefT NullT ==> a' = Null"
   149 apply (drule conf_RefTD)
   150 apply auto
   151 done
   152 
   153 lemma non_npD: "[|a' \<noteq> Null; G,h\<turnstile>a'::\<preceq>RefT t|] ==>  
   154   \<exists>a C fs. a' = Addr a \<and>  h a = Some (C,fs) \<and>  G\<turnstile>Class C\<preceq>RefT t"
   155 apply (drule conf_RefTD)
   156 apply auto
   157 done
   158 
   159 lemma non_np_objD: "!!G. [|a' \<noteq> Null; G,h\<turnstile>a'::\<preceq> Class C|] ==>  
   160   (\<exists>a C' fs. a' = Addr a \<and>  h a = Some (C',fs) \<and>  G\<turnstile>C'\<preceq>C C)"
   161 apply (fast dest: non_npD)
   162 done
   163 
   164 lemma non_np_objD' [rule_format (no_asm)]: 
   165   "a' \<noteq> Null ==> wf_prog wf_mb G ==> G,h\<turnstile>a'::\<preceq>RefT t --> 
   166   (\<exists>a C fs. a' = Addr a \<and>  h a = Some (C,fs) \<and>  G\<turnstile>Class C\<preceq>RefT t)"
   167 apply(rule_tac y = "t" in ref_ty.exhaust)
   168  apply (fast dest: conf_NullTD)
   169 apply (fast dest: non_np_objD)
   170 done
   171 
   172 lemma conf_list_gext_widen [rule_format (no_asm)]: 
   173   "wf_prog wf_mb G ==> \<forall>Ts Ts'. list_all2 (conf G h) vs Ts --> 
   174   list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') Ts Ts' -->  list_all2 (conf G h) vs Ts'"
   175 apply(induct_tac "vs")
   176  apply(clarsimp)
   177 apply(clarsimp)
   178 apply(frule list_all2_lengthD [THEN sym])
   179 apply(simp (no_asm_use) add: length_Suc_conv)
   180 apply(safe)
   181 apply(frule list_all2_lengthD [THEN sym])
   182 apply(simp (no_asm_use) add: length_Suc_conv)
   183 apply(clarify)
   184 apply(fast elim: conf_widen)
   185 done
   186 
   187 
   188 section "lconf"
   189 
   190 lemma lconfD: "[| G,h\<turnstile>vs[::\<preceq>]Ts; Ts n = Some T |] ==> G,h\<turnstile>(the (vs n))::\<preceq>T"
   191 apply (unfold lconf_def)
   192 apply (force)
   193 done
   194 
   195 lemma lconf_hext [elim]: "[| G,h\<turnstile>l[::\<preceq>]L; h\<le>|h' |] ==> G,h'\<turnstile>l[::\<preceq>]L"
   196 apply (unfold lconf_def)
   197 apply  (fast elim: conf_hext)
   198 done
   199 
   200 lemma lconf_upd: "!!X. [| G,h\<turnstile>l[::\<preceq>]lT;  
   201   G,h\<turnstile>v::\<preceq>T; lT va = Some T |] ==> G,h\<turnstile>l(va\<mapsto>v)[::\<preceq>]lT"
   202 apply (unfold lconf_def)
   203 apply auto
   204 done
   205 
   206 lemma lconf_init_vars_lemma [rule_format (no_asm)]: 
   207   "\<forall>x. P x --> R (dv x) x ==> (\<forall>x. map_of fs f = Some x --> P x) -->  
   208   (\<forall>T. map_of fs f = Some T -->  
   209   (\<exists>v. map_of (map (\<lambda>(f,ft). (f, dv ft)) fs) f = Some v \<and>  R v T))"
   210 apply( induct_tac "fs")
   211 apply auto
   212 done
   213 
   214 lemma lconf_init_vars [intro!]: 
   215 "\<forall>n. \<forall>T. map_of fs n = Some T --> is_type G T ==> G,h\<turnstile>init_vars fs[::\<preceq>]map_of fs"
   216 apply (unfold lconf_def init_vars_def)
   217 apply auto
   218 apply( rule lconf_init_vars_lemma)
   219 apply(   erule_tac [3] asm_rl)
   220 apply(  intro strip)
   221 apply(  erule defval_conf)
   222 apply auto
   223 done
   224 
   225 lemma 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)"
   226 apply (unfold lconf_def)
   227 apply auto
   228 done
   229 
   230 lemma lconf_ext_list [rule_format (no_asm)]: 
   231   "G,h\<turnstile>l[::\<preceq>]L ==> \<forall>vs Ts. distinct vns --> length Ts = length vns --> 
   232   list_all2 (\<lambda>v T. G,h\<turnstile>v::\<preceq>T) vs Ts --> G,h\<turnstile>l(vns[\<mapsto>]vs)[::\<preceq>]L(vns[\<mapsto>]Ts)"
   233 apply (unfold lconf_def)
   234 apply( induct_tac "vns")
   235 apply(  clarsimp)
   236 apply( clarsimp)
   237 apply( frule list_all2_lengthD)
   238 apply( auto simp add: length_Suc_conv)
   239 done
   240 
   241 lemma lconf_restr: "\<lbrakk>lT vn = None; G, h \<turnstile> l [::\<preceq>] lT(vn\<mapsto>T)\<rbrakk> \<Longrightarrow> G, h \<turnstile> l [::\<preceq>] lT"
   242 apply (unfold lconf_def)
   243 apply (intro strip)
   244 apply (case_tac "n = vn")
   245 apply auto
   246 done
   247 
   248 section "oconf"
   249 
   250 lemma oconf_hext: "G,h\<turnstile>obj\<surd> ==> h\<le>|h' ==> G,h'\<turnstile>obj\<surd>"
   251 apply (unfold oconf_def)
   252 apply (fast)
   253 done
   254 
   255 lemma oconf_obj: "G,h\<turnstile>(C,fs)\<surd> =  
   256   (\<forall>T f. map_of(fields (G,C)) f = Some T --> (\<exists>v. fs f = Some v \<and>  G,h\<turnstile>v::\<preceq>T))"
   257 apply (unfold oconf_def lconf_def)
   258 apply auto
   259 done
   260 
   261 lemmas oconf_objD = oconf_obj [THEN iffD1, THEN spec, THEN spec, THEN mp]
   262 
   263 
   264 section "hconf"
   265 
   266 lemma hconfD: "[|G\<turnstile>h h\<surd>; h a = Some obj|] ==> G,h\<turnstile>obj\<surd>"
   267 apply (unfold hconf_def)
   268 apply (fast)
   269 done
   270 
   271 lemma hconfI: "\<forall>a obj. h a=Some obj --> G,h\<turnstile>obj\<surd> ==> G\<turnstile>h h\<surd>"
   272 apply (unfold hconf_def)
   273 apply (fast)
   274 done
   275 
   276 
   277 section "xconf"
   278 
   279 lemma xconf_raise_if: "xconf h x \<Longrightarrow> xconf h (raise_if b xcn x)"
   280 by (simp add: xconf_def raise_if_def)
   281 
   282 
   283 
   284 section "conforms"
   285 
   286 lemma conforms_heapD: "(x, (h, l))::\<preceq>(G, lT) ==> G\<turnstile>h h\<surd>"
   287 apply (unfold conforms_def)
   288 apply (simp)
   289 done
   290 
   291 lemma conforms_localD: "(x, (h, l))::\<preceq>(G, lT) ==> G,h\<turnstile>l[::\<preceq>]lT"
   292 apply (unfold conforms_def)
   293 apply (simp)
   294 done
   295 
   296 lemma conforms_xcptD: "(x, (h, l))::\<preceq>(G, lT) ==> xconf h x"
   297 apply (unfold conforms_def)
   298 apply (simp)
   299 done
   300 
   301 lemma conformsI: "[|G\<turnstile>h h\<surd>; G,h\<turnstile>l[::\<preceq>]lT; xconf h x|] ==> (x, (h, l))::\<preceq>(G, lT)"
   302 apply (unfold conforms_def)
   303 apply auto
   304 done
   305 
   306 lemma conforms_restr: "\<lbrakk>lT vn = None; s ::\<preceq> (G, lT(vn\<mapsto>T)) \<rbrakk> \<Longrightarrow> s ::\<preceq> (G, lT)"
   307 by (simp add: conforms_def, fast intro: lconf_restr)
   308 
   309 lemma conforms_xcpt_change: "\<lbrakk> (x, (h,l))::\<preceq> (G, lT); xconf h x \<longrightarrow> xconf h x' \<rbrakk> \<Longrightarrow> (x', (h,l))::\<preceq> (G, lT)"
   310 by (simp add: conforms_def)
   311 
   312 
   313 lemma preallocated_hext: "\<lbrakk> preallocated h; h\<le>|h'\<rbrakk> \<Longrightarrow> preallocated h'"
   314 by (simp add: preallocated_def hext_def)
   315 
   316 lemma xconf_hext: "\<lbrakk> xconf h vo; h\<le>|h'\<rbrakk> \<Longrightarrow> xconf h' vo"
   317 by (simp add: xconf_def preallocated_def hext_def)
   318 
   319 lemma conforms_hext: "[|(x,(h,l))::\<preceq>(G,lT); h\<le>|h'; G\<turnstile>h h'\<surd> |] 
   320   ==> (x,(h',l))::\<preceq>(G,lT)"
   321 by( fast dest: conforms_localD conforms_xcptD elim!: conformsI xconf_hext)
   322 
   323 
   324 lemma conforms_upd_obj: 
   325   "[|(x,(h,l))::\<preceq>(G, lT); G,h(a\<mapsto>obj)\<turnstile>obj\<surd>; h\<le>|h(a\<mapsto>obj)|] 
   326   ==> (x,(h(a\<mapsto>obj),l))::\<preceq>(G, lT)"
   327 apply(rule conforms_hext)
   328 apply  auto
   329 apply(rule hconfI)
   330 apply(drule conforms_heapD)
   331 apply(tactic {* auto_tac (HOL_cs addEs [@{thm oconf_hext}] 
   332                 addDs [@{thm hconfD}], @{simpset} delsimps [@{thm split_paired_All}]) *})
   333 done
   334 
   335 lemma conforms_upd_local: 
   336 "[|(x,(h, l))::\<preceq>(G, lT); G,h\<turnstile>v::\<preceq>T; lT va = Some T|] 
   337   ==> (x,(h, l(va\<mapsto>v)))::\<preceq>(G, lT)"
   338 apply (unfold conforms_def)
   339 apply( auto elim: lconf_upd)
   340 done
   341 
   342 end