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