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