src/HOL/MicroJava/BV/Correct.thy
author webertj
Mon Mar 07 19:30:53 2005 +0100 (2005-03-07)
changeset 15584 3478bb4f93ff
parent 13681 06cce9be31a4
child 16417 9bc16273c2d4
permissions -rw-r--r--
refute_params: default value itself=1 added (for type classes)
kleing@12545
     1
nipkow@8011
     2
(*  Title:      HOL/MicroJava/BV/Correct.thy
nipkow@8011
     3
    ID:         $Id$
kleing@12516
     4
    Author:     Cornelia Pusch, Gerwin Klein
nipkow@8011
     5
    Copyright   1999 Technische Universitaet Muenchen
nipkow@8011
     6
nipkow@8011
     7
The invariant for the type safety proof.
nipkow@8011
     8
*)
nipkow@8011
     9
kleing@12911
    10
header {* \isaheader{BV Type Safety Invariant} *}
kleing@9757
    11
kleing@12774
    12
theory Correct = BVSpec + JVMExec:
nipkow@8011
    13
nipkow@8011
    14
constdefs
kleing@13006
    15
  approx_val :: "[jvm_prog,aheap,val,ty err] \<Rightarrow> bool"
kleing@13006
    16
  "approx_val G h v any == case any of Err \<Rightarrow> True | OK T \<Rightarrow> G,h\<turnstile>v::\<preceq>T"
nipkow@8011
    17
kleing@13006
    18
  approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \<Rightarrow> bool"
kleing@10056
    19
  "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
kleing@10056
    20
kleing@13006
    21
  approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \<Rightarrow> bool"
kleing@10496
    22
  "approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)"
kleing@9757
    23
kleing@13006
    24
  correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] \<Rightarrow> frame \<Rightarrow> bool"
kleing@10056
    25
  "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
kleing@10056
    26
                         approx_stk G hp stk ST  \<and> approx_loc G hp loc LT \<and> 
kleing@10056
    27
                         pc < length ins \<and> length loc=length(snd sig)+maxl+1"
nipkow@8011
    28
nipkow@8011
    29
nipkow@8011
    30
consts
kleing@13006
    31
 correct_frames  :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \<Rightarrow> bool"
nipkow@8011
    32
primrec
nipkow@8045
    33
"correct_frames G hp phi rT0 sig0 [] = True"
nipkow@8011
    34
nipkow@8045
    35
"correct_frames G hp phi rT0 sig0 (f#frs) =
kleing@11252
    36
  (let (stk,loc,C,sig,pc) = f in
kleing@12516
    37
  (\<exists>ST LT rT maxs maxl ins et.
kleing@10625
    38
    phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and> 
kleing@12516
    39
    method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and>
kleing@12516
    40
  (\<exists>C' mn pTs. ins!pc = (Invoke C' mn pTs) \<and> 
kleing@9757
    41
         (mn,pTs) = sig0 \<and> 
kleing@9757
    42
         (\<exists>apTs D ST' LT'.
kleing@12516
    43
         (phi C sig)!pc = Some ((rev apTs) @ (Class D) # ST', LT') \<and>
kleing@9757
    44
         length apTs = length pTs \<and>
kleing@12516
    45
         (\<exists>D' rT' maxs' maxl' ins' et'.
kleing@12516
    46
           method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins',et')) \<and>
kleing@9757
    47
           G \<turnstile> rT0 \<preceq> rT') \<and>
kleing@12516
    48
   correct_frame G hp (ST, LT) maxl ins f \<and> 
kleing@12516
    49
   correct_frames G hp phi rT sig frs))))"
nipkow@8011
    50
nipkow@8011
    51
nipkow@8011
    52
constdefs
kleing@13006
    53
 correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
oheimb@11372
    54
                  ("_,_ |-JVM _ [ok]"  [51,51] 50)
kleing@10042
    55
"correct_state G phi == \<lambda>(xp,hp,frs).
nipkow@8011
    56
   case xp of
kleing@13006
    57
     None \<Rightarrow> (case frs of
kleing@13006
    58
             [] \<Rightarrow> True
kleing@13006
    59
             | (f#fs) \<Rightarrow> G\<turnstile>h hp\<surd> \<and> preallocated hp \<and> 
kleing@12516
    60
      (let (stk,loc,C,sig,pc) = f
kleing@12516
    61
             in
kleing@12516
    62
                         \<exists>rT maxs maxl ins et s.
kleing@10625
    63
                         is_class G C \<and>
kleing@12516
    64
                         method (G,C) sig = Some(C,rT,(maxs,maxl,ins,et)) \<and>
kleing@9757
    65
                         phi C sig ! pc = Some s \<and>
kleing@12516
    66
       correct_frame G hp s maxl ins f \<and> 
kleing@12516
    67
             correct_frames G hp phi rT sig fs))
kleing@13006
    68
   | Some x \<Rightarrow> frs = []" 
kleing@9757
    69
kleing@9757
    70
oheimb@11372
    71
syntax (xsymbols)
kleing@13006
    72
 correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
oheimb@11372
    73
                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
kleing@10060
    74
kleing@11252
    75
kleing@11252
    76
lemma sup_ty_opt_OK:
kleing@11252
    77
  "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
kleing@11252
    78
  apply (cases X)
kleing@11252
    79
  apply auto
kleing@11252
    80
  done
kleing@11252
    81
kleing@11252
    82
kleing@11085
    83
section {* approx-val *}
kleing@9757
    84
kleing@11252
    85
lemma approx_val_Err [simp,intro!]:
kleing@9757
    86
  "approx_val G hp x Err"
kleing@11252
    87
  by (simp add: approx_val_def)
kleing@9757
    88
kleing@11252
    89
lemma approx_val_OK [iff]: 
kleing@11252
    90
  "approx_val G hp x (OK T) = (G,hp \<turnstile> x ::\<preceq> T)"
kleing@11252
    91
  by (simp add: approx_val_def)
kleing@9757
    92
kleing@11252
    93
lemma approx_val_Null [simp,intro!]:
kleing@11252
    94
  "approx_val G hp Null (OK (RefT x))"
kleing@11252
    95
  by (auto simp add: approx_val_def)
kleing@9757
    96
kleing@11252
    97
lemma approx_val_sup_heap:
kleing@11252
    98
  "\<lbrakk> approx_val G hp v T; hp \<le>| hp' \<rbrakk> \<Longrightarrow> approx_val G hp' v T"
kleing@11252
    99
  by (cases T) (blast intro: conf_hext)+
kleing@9757
   100
kleing@11252
   101
lemma approx_val_heap_update:
kleing@13006
   102
  "\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> 
kleing@13006
   103
  \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T"
kleing@11252
   104
  by (cases v, auto simp add: obj_ty_def conf_def)
kleing@9757
   105
kleing@11252
   106
lemma approx_val_widen:
kleing@11252
   107
  "\<lbrakk> approx_val G hp v T; G \<turnstile> T <=o T'; wf_prog wt G \<rbrakk>
kleing@11252
   108
  \<Longrightarrow> approx_val G hp v T'"
kleing@11252
   109
  by (cases T', auto simp add: sup_ty_opt_OK intro: conf_widen)
kleing@9757
   110
kleing@11085
   111
section {* approx-loc *}
kleing@9757
   112
kleing@11252
   113
lemma approx_loc_Nil [simp,intro!]:
kleing@11252
   114
  "approx_loc G hp [] []"
kleing@11252
   115
  by (simp add: approx_loc_def)
kleing@11252
   116
kleing@9757
   117
lemma approx_loc_Cons [iff]:
kleing@11252
   118
  "approx_loc G hp (l#ls) (L#LT) = 
kleing@11252
   119
  (approx_val G hp l L \<and> approx_loc G hp ls LT)"
kleing@9757
   120
by (simp add: approx_loc_def)
kleing@9757
   121
kleing@11252
   122
lemma approx_loc_nth:
kleing@11252
   123
  "\<lbrakk> approx_loc G hp loc LT; n < length LT \<rbrakk>
kleing@11252
   124
  \<Longrightarrow> approx_val G hp (loc!n) (LT!n)"
kleing@11252
   125
  by (simp add: approx_loc_def list_all2_conv_all_nth)
kleing@11252
   126
kleing@11252
   127
lemma approx_loc_imp_approx_val_sup:
kleing@11252
   128
  "\<lbrakk>approx_loc G hp loc LT; n < length LT; LT ! n = OK T; G \<turnstile> T \<preceq> T'; wf_prog wt G\<rbrakk> 
kleing@11252
   129
  \<Longrightarrow> G,hp \<turnstile> (loc!n) ::\<preceq> T'"
kleing@11252
   130
  apply (drule approx_loc_nth, assumption) 
kleing@11252
   131
  apply simp
kleing@11252
   132
  apply (erule conf_widen, assumption+)
kleing@11252
   133
  done
kleing@11252
   134
kleing@11252
   135
lemma approx_loc_conv_all_nth:
kleing@11252
   136
  "approx_loc G hp loc LT = 
kleing@11252
   137
  (length loc = length LT \<and> (\<forall>n < length loc. approx_val G hp (loc!n) (LT!n)))"
kleing@11252
   138
  by (simp add: approx_loc_def list_all2_conv_all_nth)
kleing@11252
   139
kleing@11252
   140
lemma approx_loc_sup_heap:
kleing@11252
   141
  "\<lbrakk> approx_loc G hp loc LT; hp \<le>| hp' \<rbrakk>
kleing@11252
   142
  \<Longrightarrow> approx_loc G hp' loc LT"
kleing@11252
   143
  apply (clarsimp simp add: approx_loc_conv_all_nth)
kleing@11252
   144
  apply (blast intro: approx_val_sup_heap)
kleing@11252
   145
  done
kleing@11252
   146
kleing@11252
   147
lemma approx_loc_widen:
kleing@11252
   148
  "\<lbrakk> approx_loc G hp loc LT; G \<turnstile> LT <=l LT'; wf_prog wt G \<rbrakk>
kleing@11252
   149
  \<Longrightarrow> approx_loc G hp loc LT'"
kleing@11252
   150
apply (unfold Listn.le_def lesub_def sup_loc_def)
kleing@11252
   151
apply (simp (no_asm_use) only: list_all2_conv_all_nth approx_loc_conv_all_nth)
kleing@11252
   152
apply (simp (no_asm_simp))
kleing@11252
   153
apply clarify
kleing@11252
   154
apply (erule allE, erule impE) 
kleing@11252
   155
 apply simp
kleing@11252
   156
apply (erule approx_val_widen)
kleing@11252
   157
 apply simp
kleing@11252
   158
apply assumption
kleing@10056
   159
done
kleing@9757
   160
kleing@13052
   161
lemma loc_widen_Err [dest]:
kleing@13052
   162
  "\<And>XT. G \<turnstile> replicate n Err <=l XT \<Longrightarrow> XT = replicate n Err"
kleing@13052
   163
  by (induct n) auto
kleing@13052
   164
  
kleing@13052
   165
lemma approx_loc_Err [iff]:
kleing@13052
   166
  "approx_loc G hp (replicate n v) (replicate n Err)"
kleing@13052
   167
  by (induct n) auto
kleing@13052
   168
kleing@11252
   169
lemma approx_loc_subst:
kleing@11252
   170
  "\<lbrakk> approx_loc G hp loc LT; approx_val G hp x X \<rbrakk>
kleing@11252
   171
  \<Longrightarrow> approx_loc G hp (loc[idx:=x]) (LT[idx:=X])"
kleing@9757
   172
apply (unfold approx_loc_def list_all2_def)
kleing@9757
   173
apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
kleing@10056
   174
done
kleing@9757
   175
kleing@11252
   176
lemma approx_loc_append:
kleing@11252
   177
  "length l1=length L1 \<Longrightarrow>
kleing@10056
   178
  approx_loc G hp (l1@l2) (L1@L2) = 
kleing@10056
   179
  (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
kleing@11252
   180
  apply (unfold approx_loc_def list_all2_def)
kleing@11252
   181
  apply (simp cong: conj_cong)
kleing@11252
   182
  apply blast
kleing@11252
   183
  done
kleing@9757
   184
kleing@11085
   185
section {* approx-stk *}
kleing@9757
   186
kleing@9757
   187
lemma approx_stk_rev_lem:
kleing@9757
   188
  "approx_stk G hp (rev s) (rev t) = approx_stk G hp s t"
kleing@11252
   189
  apply (unfold approx_stk_def approx_loc_def)
kleing@11252
   190
  apply (simp add: rev_map [THEN sym])
kleing@11252
   191
  done
kleing@9757
   192
kleing@9757
   193
lemma approx_stk_rev:
kleing@9757
   194
  "approx_stk G hp (rev s) t = approx_stk G hp s (rev t)"
kleing@11252
   195
  by (auto intro: subst [OF approx_stk_rev_lem])
kleing@9757
   196
kleing@11252
   197
lemma approx_stk_sup_heap:
kleing@11252
   198
  "\<lbrakk> approx_stk G hp stk ST; hp \<le>| hp' \<rbrakk> \<Longrightarrow> approx_stk G hp' stk ST"
kleing@11252
   199
  by (auto intro: approx_loc_sup_heap simp add: approx_stk_def)
kleing@9757
   200
kleing@11252
   201
lemma approx_stk_widen:
kleing@11252
   202
  "\<lbrakk> approx_stk G hp stk ST; G \<turnstile> map OK ST <=l map OK ST'; wf_prog wt G \<rbrakk>
kleing@11252
   203
  \<Longrightarrow> approx_stk G hp stk ST'" 
kleing@11252
   204
  by (auto elim: approx_loc_widen simp add: approx_stk_def)
kleing@9757
   205
kleing@9757
   206
lemma approx_stk_Nil [iff]:
kleing@9757
   207
  "approx_stk G hp [] []"
kleing@11252
   208
  by (simp add: approx_stk_def)
kleing@9757
   209
kleing@9757
   210
lemma approx_stk_Cons [iff]:
kleing@11252
   211
  "approx_stk G hp (x#stk) (S#ST) = 
kleing@11252
   212
  (approx_val G hp x (OK S) \<and> approx_stk G hp stk ST)"
kleing@11252
   213
  by (simp add: approx_stk_def)
kleing@9757
   214
kleing@9757
   215
lemma approx_stk_Cons_lemma [iff]:
kleing@9757
   216
  "approx_stk G hp stk (S#ST') = 
kleing@10496
   217
  (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (OK S) \<and> approx_stk G hp stk' ST')"
kleing@11252
   218
  by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
kleing@11252
   219
kleing@11252
   220
lemma approx_stk_append:
kleing@11252
   221
  "approx_stk G hp stk (S@S') \<Longrightarrow>
kleing@11252
   222
  (\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length S' \<and> 
kleing@11252
   223
            approx_stk G hp s S \<and> approx_stk G hp stk' S')"
kleing@11252
   224
  by (simp add: list_all2_append2 approx_stk_def approx_loc_def)
kleing@9757
   225
kleing@11252
   226
lemma approx_stk_all_widen:
kleing@11252
   227
  "\<lbrakk> approx_stk G hp stk ST; \<forall>x \<in> set (zip ST ST'). x \<in> widen G; length ST = length ST'; wf_prog wt G \<rbrakk> 
kleing@11252
   228
  \<Longrightarrow> approx_stk G hp stk ST'"
kleing@11252
   229
apply (unfold approx_stk_def)
kleing@11252
   230
apply (clarsimp simp add: approx_loc_conv_all_nth all_set_conv_all_nth)
kleing@11252
   231
apply (erule allE, erule impE, assumption)
kleing@11252
   232
apply (erule allE, erule impE, assumption)
kleing@11252
   233
apply (erule conf_widen, assumption+)
kleing@11252
   234
done
kleing@9757
   235
kleing@11085
   236
section {* oconf *}
kleing@9757
   237
kleing@11252
   238
lemma oconf_field_update:
kleing@13006
   239
  "\<lbrakk>map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> \<rbrakk>
kleing@13006
   240
  \<Longrightarrow> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>"
kleing@11252
   241
  by (simp add: oconf_def lconf_def)
kleing@9757
   242
kleing@11252
   243
lemma oconf_newref:
kleing@11252
   244
  "\<lbrakk>hp oref = None; G,hp \<turnstile> obj \<surd>; G,hp \<turnstile> obj' \<surd>\<rbrakk> \<Longrightarrow> G,hp(oref\<mapsto>obj') \<turnstile> obj \<surd>"
kleing@11252
   245
  apply (unfold oconf_def lconf_def)
kleing@11252
   246
  apply simp
kleing@11252
   247
  apply (blast intro: conf_hext hext_new)
kleing@11252
   248
  done
kleing@9757
   249
kleing@11252
   250
lemma oconf_heap_update:
kleing@11252
   251
  "\<lbrakk> hp a = Some obj'; obj_ty obj' = obj_ty obj''; G,hp\<turnstile>obj\<surd> \<rbrakk>
kleing@11252
   252
  \<Longrightarrow> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>"
kleing@11252
   253
  apply (unfold oconf_def lconf_def)
kleing@11252
   254
  apply (fastsimp intro: approx_val_heap_update)
kleing@11252
   255
  done
kleing@9757
   256
kleing@11085
   257
section {* hconf *}
kleing@9757
   258
kleing@11252
   259
lemma hconf_newref:
kleing@11252
   260
  "\<lbrakk> hp oref = None; G\<turnstile>h hp\<surd>; G,hp\<turnstile>obj\<surd> \<rbrakk> \<Longrightarrow> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>"
kleing@11252
   261
  apply (simp add: hconf_def)
kleing@11252
   262
  apply (fast intro: oconf_newref)
kleing@11252
   263
  done
kleing@9757
   264
kleing@11252
   265
lemma hconf_field_update:
kleing@11252
   266
  "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
kleing@11252
   267
     G,hp\<turnstile>v::\<preceq>T; G\<turnstile>h hp\<surd> \<rbrakk> 
kleing@11252
   268
  \<Longrightarrow> G\<turnstile>h hp(a \<mapsto> (oT, fs(X\<mapsto>v)))\<surd>"
kleing@11252
   269
  apply (simp add: hconf_def)
kleing@11252
   270
  apply (fastsimp intro: oconf_heap_update oconf_field_update 
kleing@11252
   271
                  simp add: obj_ty_def)
kleing@11252
   272
  done
kleing@9757
   273
kleing@12545
   274
section {* preallocated *}
kleing@12545
   275
kleing@12545
   276
lemma preallocated_field_update:
kleing@12545
   277
  "\<lbrakk> map_of (fields (G, oT)) X = Some T; hp a = Some(oT,fs); 
kleing@12545
   278
     G\<turnstile>h hp\<surd>; preallocated hp \<rbrakk> 
kleing@12545
   279
  \<Longrightarrow> preallocated (hp(a \<mapsto> (oT, fs(X\<mapsto>v))))"
kleing@12545
   280
  apply (unfold preallocated_def)
kleing@12545
   281
  apply (rule allI)
kleing@12545
   282
  apply (erule_tac x=x in allE)
kleing@12545
   283
  apply simp
kleing@12545
   284
  apply (rule ccontr)  
kleing@12545
   285
  apply (unfold hconf_def)
kleing@12545
   286
  apply (erule allE, erule allE, erule impE, assumption)
kleing@12545
   287
  apply (unfold oconf_def lconf_def)
kleing@12545
   288
  apply (simp del: split_paired_All)
kleing@12545
   289
  done  
kleing@12545
   290
kleing@12545
   291
kleing@13052
   292
lemma 
kleing@13052
   293
  assumes none: "hp oref = None" and alloc: "preallocated hp"
kleing@13052
   294
  shows preallocated_newref: "preallocated (hp(oref\<mapsto>obj))"
kleing@13052
   295
proof (cases oref)
kleing@13052
   296
  case (XcptRef x) 
kleing@13052
   297
  with none alloc have "False" by (auto elim: preallocatedE [of _ x])
kleing@13052
   298
  thus ?thesis ..
kleing@13052
   299
next
kleing@13052
   300
  case (Loc l)
kleing@13052
   301
  with alloc show ?thesis by (simp add: preallocated_def)
kleing@13052
   302
qed
kleing@13052
   303
  
kleing@11085
   304
section {* correct-frames *}
kleing@9757
   305
kleing@9757
   306
lemmas [simp del] = fun_upd_apply
kleing@9757
   307
kleing@11252
   308
lemma correct_frames_field_update [rule_format]:
kleing@11252
   309
  "\<forall>rT C sig. 
kleing@13006
   310
  correct_frames G hp phi rT sig frs \<longrightarrow> 
kleing@13006
   311
  hp a = Some (C,fs) \<longrightarrow> 
kleing@13006
   312
  map_of (fields (G, C)) fl = Some fd \<longrightarrow> 
kleing@10042
   313
  G,hp\<turnstile>v::\<preceq>fd 
kleing@13006
   314
  \<longrightarrow> correct_frames G (hp(a \<mapsto> (C, fs(fl\<mapsto>v)))) phi rT sig frs";
kleing@9757
   315
apply (induct frs)
kleing@9757
   316
 apply simp
kleing@10920
   317
apply clarify
kleing@11252
   318
apply (simp (no_asm_use))
kleing@10920
   319
apply clarify
kleing@10920
   320
apply (unfold correct_frame_def)
kleing@10920
   321
apply (simp (no_asm_use))
kleing@11252
   322
apply clarify
kleing@9757
   323
apply (intro exI conjI)
kleing@11252
   324
    apply assumption+
kleing@11252
   325
   apply (erule approx_stk_sup_heap)
kleing@11252
   326
   apply (erule hext_upd_obj)
kleing@11252
   327
  apply (erule approx_loc_sup_heap)
kleing@11252
   328
  apply (erule hext_upd_obj)
kleing@11252
   329
 apply assumption+
kleing@11252
   330
apply blast
kleing@10056
   331
done
kleing@9757
   332
kleing@11252
   333
lemma correct_frames_newref [rule_format]:
kleing@11252
   334
  "\<forall>rT C sig. 
kleing@11252
   335
  hp x = None \<longrightarrow> 
kleing@11252
   336
  correct_frames G hp phi rT sig frs \<longrightarrow>
kleing@13681
   337
  correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs"
kleing@9757
   338
apply (induct frs)
kleing@9757
   339
 apply simp
kleing@11252
   340
apply clarify
kleing@11252
   341
apply (simp (no_asm_use))
kleing@11252
   342
apply clarify
kleing@11252
   343
apply (unfold correct_frame_def)
kleing@11252
   344
apply (simp (no_asm_use))
kleing@11252
   345
apply clarify
kleing@9757
   346
apply (intro exI conjI)
kleing@11252
   347
    apply assumption+
kleing@11252
   348
   apply (erule approx_stk_sup_heap)
kleing@11252
   349
   apply (erule hext_new)
kleing@11252
   350
  apply (erule approx_loc_sup_heap)
kleing@11252
   351
  apply (erule hext_new)
kleing@11252
   352
 apply assumption+
kleing@11252
   353
apply blast
kleing@10056
   354
done
nipkow@8011
   355
nipkow@8011
   356
end