src/HOL/MicroJava/BV/BVExample.thy
author wenzelm
Thu Mar 07 23:41:30 2002 +0100 (2002-03-07)
changeset 13043 ad1828b479b7
parent 13006 51c5f3f11d16
child 13052 3bf41c474a88
permissions -rw-r--r--
renamed nat_number_of to nat_number (avoid clash with separate theorem);
kleing@12951
     1
(*  Title:      HOL/MicroJava/BV/BVExample.thy
kleing@12951
     2
    ID:         $Id$
kleing@12951
     3
    Author:     Gerwin Klein
kleing@12951
     4
*)
kleing@12951
     5
kleing@12972
     6
header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
kleing@12951
     7
kleing@12951
     8
theory BVExample = JVMListExample + Correct:
kleing@12951
     9
kleing@12972
    10
text {*
kleing@12972
    11
  This theory shows type correctness of the example program in section 
kleing@12972
    12
  \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
kleing@12972
    13
  explicitly providing a welltyping. It also shows that the start
kleing@12972
    14
  state of the program conforms to the welltyping; hence type safe
kleing@12972
    15
  execution is guaranteed.
kleing@12972
    16
*}
kleing@12972
    17
kleing@12951
    18
section "Setup"
kleing@12951
    19
text {*
kleing@12951
    20
  Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
kleing@12951
    21
  anonymous, we describe distinctness of names in the example by axioms:
kleing@12951
    22
*}
kleing@12951
    23
axioms 
kleing@12951
    24
  distinct_classes: "list_nam \<noteq> test_nam"
kleing@12951
    25
  distinct_fields:  "val_nam \<noteq> next_nam"
kleing@12951
    26
kleing@12951
    27
text {* Shorthands for definitions we will have to use often in the
kleing@12951
    28
proofs below: *}
kleing@12951
    29
lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def
kleing@12951
    30
lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
kleing@12951
    31
                     OutOfMemoryC_def ClassCastC_def
kleing@12951
    32
lemmas class_defs  = list_class_def test_class_def
kleing@12951
    33
kleing@12951
    34
text {* These auxiliary proofs are for efficiency: class lookup,
kleing@12951
    35
subclass relation, method and field lookup are computed only once:
kleing@12951
    36
*}
kleing@12951
    37
lemma class_Object [simp]:
kleing@12951
    38
  "class E Object = Some (arbitrary, [],[])"
kleing@12951
    39
  by (simp add: class_def system_defs E_def)
kleing@12951
    40
kleing@12951
    41
lemma class_NullPointer [simp]:
kleing@12951
    42
  "class E (Xcpt NullPointer) = Some (Object, [], [])"
kleing@12951
    43
  by (simp add: class_def system_defs E_def)
kleing@12951
    44
kleing@12951
    45
lemma class_OutOfMemory [simp]:
kleing@12951
    46
  "class E (Xcpt OutOfMemory) = Some (Object, [], [])"
kleing@12951
    47
  by (simp add: class_def system_defs E_def)
kleing@12951
    48
kleing@12951
    49
lemma class_ClassCast [simp]:
kleing@12951
    50
  "class E (Xcpt ClassCast) = Some (Object, [], [])"
kleing@12951
    51
  by (simp add: class_def system_defs E_def)
kleing@12951
    52
kleing@12951
    53
lemma class_list [simp]:
kleing@12951
    54
  "class E list_name = Some list_class"
kleing@12951
    55
  by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
kleing@12951
    56
 
kleing@12951
    57
lemma class_test [simp]:
kleing@12951
    58
  "class E test_name = Some test_class"
kleing@12951
    59
  by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
kleing@12951
    60
kleing@12951
    61
lemma E_classes [simp]:
kleing@12951
    62
  "{C. is_class E C} = {list_name, test_name, Xcpt NullPointer, 
kleing@12951
    63
                        Xcpt ClassCast, Xcpt OutOfMemory, Object}"
kleing@12951
    64
  by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
kleing@12951
    65
kleing@12951
    66
text {* The subclass releation spelled out: *}
kleing@12951
    67
lemma subcls1:
kleing@12951
    68
  "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
kleing@12951
    69
                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
kleing@12951
    70
  apply (simp add: subcls1_def2)
kleing@12951
    71
  apply (simp add: name_defs class_defs system_defs E_def class_def)
kleing@12951
    72
  apply (auto split: split_if_asm)
kleing@12951
    73
  done
kleing@12951
    74
kleing@12951
    75
text {* The subclass relation is acyclic; hence its converse is well founded: *}
kleing@12951
    76
lemma notin_rtrancl:
kleing@12951
    77
  "(a,b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a,y) \<notin> r) \<Longrightarrow> False"
kleing@12951
    78
  by (auto elim: converse_rtranclE)  
kleing@12951
    79
kleing@12951
    80
lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
kleing@12951
    81
  apply (rule acyclicI)
kleing@12951
    82
  apply (simp add: subcls1)
kleing@12951
    83
  apply (auto dest!: tranclD)
kleing@12951
    84
  apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
kleing@12951
    85
  done
kleing@12951
    86
kleing@12951
    87
lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
kleing@12951
    88
  apply (rule finite_acyclic_wf_converse)
kleing@12951
    89
  apply (simp add: subcls1)
kleing@12951
    90
  apply (rule acyclic_subcls1_E)
kleing@12951
    91
  done  
kleing@12951
    92
kleing@12951
    93
text {* Method and field lookup: *}
kleing@12951
    94
lemma method_Object [simp]:
kleing@12951
    95
  "method (E, Object) = empty"
kleing@12951
    96
  by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
kleing@12951
    97
kleing@12951
    98
lemma method_append [simp]:
kleing@12951
    99
  "method (E, list_name) (append_name, [Class list_name]) =
kleing@12951
   100
  Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"
kleing@12951
   101
  apply (insert class_list)
kleing@12951
   102
  apply (unfold list_class_def)
kleing@12951
   103
  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   104
  apply simp
kleing@12951
   105
  done
kleing@12951
   106
kleing@12951
   107
lemma method_makelist [simp]:
kleing@12951
   108
  "method (E, test_name) (makelist_name, []) = 
kleing@12951
   109
  Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"
kleing@12951
   110
  apply (insert class_test)
kleing@12951
   111
  apply (unfold test_class_def)
kleing@12951
   112
  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   113
  apply simp
kleing@12951
   114
  done
kleing@12951
   115
kleing@12951
   116
lemma field_val [simp]:
kleing@12951
   117
  "field (E, list_name) val_name = Some (list_name, PrimT Integer)"
kleing@12951
   118
  apply (unfold field_def)
kleing@12951
   119
  apply (insert class_list)
kleing@12951
   120
  apply (unfold list_class_def)
kleing@12951
   121
  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   122
  apply simp
kleing@12951
   123
  done
kleing@12951
   124
kleing@12951
   125
lemma field_next [simp]:
kleing@12951
   126
  "field (E, list_name) next_name = Some (list_name, Class list_name)"
kleing@12951
   127
  apply (unfold field_def)
kleing@12951
   128
  apply (insert class_list)
kleing@12951
   129
  apply (unfold list_class_def)
kleing@12951
   130
  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   131
  apply (simp add: name_defs distinct_fields [symmetric])
kleing@12951
   132
  done
kleing@12951
   133
kleing@12951
   134
lemma [simp]: "fields (E, Object) = []"
kleing@12951
   135
   by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])
kleing@12951
   136
 
kleing@12951
   137
lemma [simp]: "fields (E, Xcpt NullPointer) = []"
kleing@12951
   138
  by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])
kleing@12951
   139
kleing@12951
   140
lemma [simp]: "fields (E, Xcpt ClassCast) = []"
kleing@12951
   141
  by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])
kleing@12951
   142
kleing@12951
   143
lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"
kleing@12951
   144
  by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])
kleing@12951
   145
kleing@12951
   146
lemma [simp]: "fields (E, test_name) = []"
kleing@12951
   147
  apply (insert class_test)
kleing@12951
   148
  apply (unfold test_class_def)
kleing@12951
   149
  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   150
  apply simp
kleing@12951
   151
  done
kleing@12951
   152
kleing@12951
   153
lemmas [simp] = is_class_def
kleing@12951
   154
kleing@12951
   155
text {*
kleing@12951
   156
  The next definition and three proof rules implement an algorithm to
kleing@12951
   157
  enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} 
kleing@12951
   158
  transforms a goal of the form
kleing@12951
   159
  @{prop [display] "pc < n \<Longrightarrow> P pc"} 
kleing@12951
   160
  into a series of goals
kleing@12951
   161
  @{prop [display] "P 0"} 
kleing@12951
   162
  @{prop [display] "P (Suc 0)"} 
kleing@12951
   163
kleing@12951
   164
  @{text "\<dots>"}
kleing@12951
   165
kleing@12951
   166
  @{prop [display] "P n"} 
kleing@12951
   167
*}
kleing@12951
   168
constdefs 
kleing@12951
   169
  intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')")
kleing@12951
   170
  "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
kleing@12951
   171
kleing@12951
   172
lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
kleing@12951
   173
  by (simp add: intervall_def)
kleing@12951
   174
kleing@12951
   175
lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
kleing@12951
   176
  apply (cases "x=n0")
kleing@12951
   177
  apply (auto simp add: intervall_def) 
kleing@12951
   178
  apply arith
kleing@12951
   179
  done
kleing@12951
   180
kleing@12951
   181
lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" 
kleing@12951
   182
  by (unfold intervall_def) arith
kleing@12951
   183
kleing@12951
   184
kleing@12951
   185
section "Program structure"
kleing@12951
   186
kleing@12951
   187
text {*
kleing@12951
   188
  The program is structurally wellformed:
kleing@12951
   189
*}
kleing@12951
   190
lemma wf_struct:
kleing@12951
   191
  "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
kleing@12951
   192
proof -
kleing@12951
   193
  have "unique E" 
kleing@12951
   194
    by (simp add: system_defs E_def class_defs name_defs distinct_classes)
kleing@12951
   195
  moreover
kleing@12951
   196
  have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def)
kleing@12951
   197
  hence "wf_syscls E" by (rule wf_syscls)
kleing@12951
   198
  moreover
kleing@12951
   199
  have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)
kleing@12951
   200
  moreover
kleing@12951
   201
  have "wf_cdecl ?mb E NullPointerC" 
kleing@12951
   202
    by (auto elim: notin_rtrancl 
kleing@12951
   203
            simp add: wf_cdecl_def name_defs NullPointerC_def subcls1)
kleing@12951
   204
  moreover
kleing@12951
   205
  have "wf_cdecl ?mb E ClassCastC" 
kleing@12951
   206
    by (auto elim: notin_rtrancl 
kleing@12951
   207
            simp add: wf_cdecl_def name_defs ClassCastC_def subcls1)
kleing@12951
   208
  moreover
kleing@12951
   209
  have "wf_cdecl ?mb E OutOfMemoryC" 
kleing@12951
   210
    by (auto elim: notin_rtrancl 
kleing@12951
   211
            simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1)
kleing@12951
   212
  moreover
kleing@12951
   213
  have "wf_cdecl ?mb E (list_name, list_class)"
kleing@12951
   214
    apply (auto elim!: notin_rtrancl 
kleing@12951
   215
            simp add: wf_cdecl_def wf_fdecl_def list_class_def 
kleing@12951
   216
                      wf_mdecl_def wf_mhead_def subcls1)
kleing@12951
   217
    apply (auto simp add: name_defs distinct_classes distinct_fields)
kleing@12951
   218
    done    
kleing@12951
   219
  moreover
kleing@12951
   220
  have "wf_cdecl ?mb E (test_name, test_class)" 
kleing@12951
   221
    apply (auto elim!: notin_rtrancl 
kleing@12951
   222
            simp add: wf_cdecl_def wf_fdecl_def test_class_def 
kleing@12951
   223
                      wf_mdecl_def wf_mhead_def subcls1)
kleing@12951
   224
    apply (auto simp add: name_defs distinct_classes distinct_fields)
kleing@12951
   225
    done       
kleing@12951
   226
  ultimately
kleing@12951
   227
  show ?thesis by (simp add: wf_prog_def E_def SystemClasses_def)
kleing@12951
   228
qed
kleing@12951
   229
kleing@12951
   230
section "Welltypings"
kleing@12951
   231
text {*
kleing@12951
   232
  We show welltypings of the methods @{term append_name} in class @{term list_name}, 
kleing@12951
   233
  and @{term makelist_name} in class @{term test_name}:
kleing@12951
   234
*}
kleing@12951
   235
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
kleing@12951
   236
declare appInvoke [simp del]
kleing@12951
   237
kleing@12951
   238
constdefs
kleing@12951
   239
  phi_append :: method_type ("\<phi>\<^sub>a")
kleing@12951
   240
  "\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [ 
kleing@12951
   241
   (                                    [], [Class list_name, Class list_name]),
kleing@12951
   242
   (                     [Class list_name], [Class list_name, Class list_name]),
kleing@12951
   243
   (                     [Class list_name], [Class list_name, Class list_name]),
kleing@12951
   244
   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
kleing@12951
   245
   ([NT, Class list_name, Class list_name], [Class list_name, Class list_name]),
kleing@12951
   246
   (                     [Class list_name], [Class list_name, Class list_name]),
kleing@12951
   247
   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
kleing@12951
   248
   (                          [PrimT Void], [Class list_name, Class list_name]),
kleing@12951
   249
   (                        [Class Object], [Class list_name, Class list_name]),
kleing@12951
   250
   (                                    [], [Class list_name, Class list_name]),
kleing@12951
   251
   (                     [Class list_name], [Class list_name, Class list_name]),
kleing@12951
   252
   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
kleing@12951
   253
   (                                    [], [Class list_name, Class list_name]),
kleing@12951
   254
   (                          [PrimT Void], [Class list_name, Class list_name])]"
kleing@12951
   255
kleing@12951
   256
lemma wt_append [simp]:
kleing@12951
   257
  "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
kleing@12951
   258
             [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
kleing@12951
   259
  apply (simp add: wt_method_def append_ins_def phi_append_def 
kleing@12951
   260
                   wt_start_def wt_instr_def)
kleing@12951
   261
  apply clarify
kleing@12951
   262
  apply (elim pc_end pc_next pc_0)
kleing@12951
   263
  apply simp
kleing@12951
   264
  apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
kleing@12951
   265
  apply simp
kleing@12951
   266
  apply simp
kleing@12951
   267
  apply (fastsimp simp add: sup_state_conv subcls1)
kleing@12951
   268
  apply simp
kleing@12951
   269
  apply (simp add: app_def xcpt_app_def)
kleing@12951
   270
  apply simp
kleing@12951
   271
  apply simp
kleing@12951
   272
  apply simp
kleing@12951
   273
  apply (simp add: match_exception_entry_def)
kleing@12951
   274
  apply (simp add: match_exception_entry_def)
kleing@12951
   275
  apply simp
kleing@12951
   276
  apply simp
kleing@12951
   277
  done
kleing@12951
   278
kleing@13006
   279
text {* Some abbreviations for readability *} 
kleing@12951
   280
syntax
kleing@12951
   281
  list :: ty 
kleing@12951
   282
  test :: ty
kleing@12951
   283
translations
kleing@12951
   284
  "list" == "Class list_name"
kleing@12951
   285
  "test" == "Class test_name"
kleing@12951
   286
kleing@12951
   287
constdefs
kleing@12951
   288
  phi_makelist :: method_type ("\<phi>\<^sub>m")
kleing@12951
   289
  "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ 
kleing@12951
   290
    (                                   [], [OK test, Err    , Err    ]),
kleing@12951
   291
    (                               [list], [OK test, Err    , Err    ]),
kleing@12951
   292
    (                         [list, list], [OK test, Err    , Err    ]),
kleing@12951
   293
    (                               [list], [OK list, Err    , Err    ]),
kleing@12951
   294
    (                [PrimT Integer, list], [OK list, Err    , Err    ]),
kleing@12951
   295
    (                                   [], [OK list, Err    , Err    ]),
kleing@12951
   296
    (                               [list], [OK list, Err    , Err    ]),
kleing@12951
   297
    (                         [list, list], [OK list, Err    , Err    ]),
kleing@12951
   298
    (                               [list], [OK list, OK list, Err    ]),
kleing@12951
   299
    (                [PrimT Integer, list], [OK list, OK list, Err    ]),
kleing@12951
   300
    (                                   [], [OK list, OK list, Err    ]),
kleing@12951
   301
    (                               [list], [OK list, OK list, Err    ]),
kleing@12951
   302
    (                         [list, list], [OK list, OK list, Err    ]),
kleing@12951
   303
    (                               [list], [OK list, OK list, OK list]),
kleing@12951
   304
    (                [PrimT Integer, list], [OK list, OK list, OK list]),
kleing@12951
   305
    (                                   [], [OK list, OK list, OK list]),
kleing@12951
   306
    (                               [list], [OK list, OK list, OK list]),
kleing@12951
   307
    (                         [list, list], [OK list, OK list, OK list]),
kleing@12951
   308
    (                         [PrimT Void], [OK list, OK list, OK list]),
kleing@12951
   309
    (                   [list, PrimT Void], [OK list, OK list, OK list]),
kleing@12951
   310
    (             [list, list, PrimT Void], [OK list, OK list, OK list]),
kleing@12951
   311
    (             [PrimT Void, PrimT Void], [OK list, OK list, OK list]),
kleing@12951
   312
    ( [PrimT Void, PrimT Void, PrimT Void], [OK list, OK list, OK list])]"
kleing@12951
   313
kleing@12951
   314
lemma wt_makelist [simp]:
kleing@12951
   315
  "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
kleing@12951
   316
  apply (simp add: wt_method_def make_list_ins_def phi_makelist_def)
wenzelm@13043
   317
  apply (simp add: wt_start_def nat_number)
kleing@12951
   318
  apply (simp add: wt_instr_def)
kleing@12951
   319
  apply clarify
kleing@12951
   320
  apply (elim pc_end pc_next pc_0)
kleing@12951
   321
  apply (simp add: match_exception_entry_def)
kleing@12951
   322
  apply simp
kleing@12951
   323
  apply simp
kleing@12951
   324
  apply simp
kleing@12951
   325
  apply (simp add: match_exception_entry_def)
kleing@12951
   326
  apply (simp add: match_exception_entry_def) 
kleing@12951
   327
  apply simp
kleing@12951
   328
  apply simp
kleing@12951
   329
  apply simp
kleing@12951
   330
  apply (simp add: match_exception_entry_def)
kleing@12951
   331
  apply (simp add: match_exception_entry_def) 
kleing@12951
   332
  apply simp
kleing@12951
   333
  apply simp
kleing@12951
   334
  apply simp
kleing@12951
   335
  apply (simp add: match_exception_entry_def)
kleing@12951
   336
  apply (simp add: match_exception_entry_def) 
kleing@12951
   337
  apply simp
kleing@12951
   338
  apply (simp add: app_def xcpt_app_def)
kleing@12951
   339
  apply simp
kleing@12951
   340
  apply simp
kleing@12951
   341
  apply (simp add: app_def xcpt_app_def)
kleing@12951
   342
  apply simp
kleing@12951
   343
  apply simp
kleing@12951
   344
  done
kleing@12951
   345
kleing@12951
   346
text {* The whole program is welltyped: *}
kleing@12951
   347
constdefs 
kleing@12951
   348
  Phi :: prog_type ("\<Phi>")
kleing@12951
   349
  "\<Phi> C sig \<equiv> if C = test_name \<and> sig = (makelist_name, []) then \<phi>\<^sub>m else
kleing@12951
   350
              if C = list_name \<and> sig = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
kleing@12951
   351
  
kleing@12951
   352
lemma wf_prog:
kleing@12951
   353
  "wt_jvm_prog E \<Phi>"
kleing@12951
   354
  apply (unfold wt_jvm_prog_def)
kleing@12951
   355
  apply (rule wf_mb'E [OF wf_struct])
kleing@12951
   356
  apply (simp add: E_def)
kleing@12951
   357
  apply clarify
kleing@12951
   358
  apply (fold E_def)
kleing@12951
   359
  apply (simp add: system_defs class_defs Phi_def)
kleing@12951
   360
  apply auto
kleing@12951
   361
  done
kleing@12951
   362
kleing@12951
   363
kleing@12951
   364
section "Conformance"
kleing@12951
   365
text {* Execution of the program will be typesafe, because its
kleing@12951
   366
  start state conforms to the welltyping: *}
kleing@12951
   367
kleing@12951
   368
lemma [simp]: "preallocated start_heap"
kleing@12951
   369
  apply (unfold start_heap_def preallocated_def)
kleing@12951
   370
  apply auto
kleing@12951
   371
  apply (case_tac x)
kleing@12951
   372
  apply auto
kleing@12951
   373
  done
kleing@12951
   374
kleing@12951
   375
lemma "E,\<Phi> \<turnstile>JVM start_state \<surd>"
kleing@12951
   376
  apply (simp add: correct_state_def start_state_def test_class_def)
kleing@12951
   377
  apply (simp add: hconf_def start_heap_def oconf_def lconf_def)
kleing@12951
   378
  apply (simp add: Phi_def phi_makelist_def)
kleing@12951
   379
  apply (simp add: correct_frame_def)
kleing@12951
   380
  apply (simp add: make_list_ins_def)
kleing@12951
   381
  apply (simp add: conf_def start_heap_def)
kleing@12951
   382
  done
kleing@12951
   383
kleing@13006
   384
end