src/HOL/MicroJava/BV/BVExample.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 40077 c8a9eaaa2f59
child 44035 322d1657c40c
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
kleing@12951
     1
(*  Title:      HOL/MicroJava/BV/BVExample.thy
kleing@12951
     2
    Author:     Gerwin Klein
kleing@12951
     3
*)
kleing@12951
     4
kleing@12972
     5
header {* \isaheader{Example Welltypings}\label{sec:BVExample} *}
kleing@12951
     6
haftmann@23022
     7
theory BVExample
wenzelm@41413
     8
imports
wenzelm@41413
     9
  "../JVM/JVMListExample"
wenzelm@41413
    10
  BVSpecTypeSafe
wenzelm@41413
    11
  JVM
wenzelm@41413
    12
  "~~/src/HOL/Library/Executable_Set"
haftmann@23022
    13
begin
kleing@12951
    14
kleing@12972
    15
text {*
kleing@12972
    16
  This theory shows type correctness of the example program in section 
kleing@12972
    17
  \ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by
kleing@12972
    18
  explicitly providing a welltyping. It also shows that the start
kleing@12972
    19
  state of the program conforms to the welltyping; hence type safe
kleing@12972
    20
  execution is guaranteed.
kleing@12972
    21
*}
kleing@12972
    22
kleing@12951
    23
section "Setup"
kleing@12951
    24
text {*
kleing@12951
    25
  Since the types @{typ cnam}, @{text vnam}, and @{text mname} are 
kleing@12951
    26
  anonymous, we describe distinctness of names in the example by axioms:
kleing@12951
    27
*}
kleing@12951
    28
axioms 
kleing@12951
    29
  distinct_classes: "list_nam \<noteq> test_nam"
kleing@12951
    30
  distinct_fields:  "val_nam \<noteq> next_nam"
kleing@12951
    31
kleing@13101
    32
text {* Abbreviations for definitions we will have to use often in the
kleing@12951
    33
proofs below: *}
kleing@13101
    34
lemmas name_defs   = list_name_def test_name_def val_name_def next_name_def 
kleing@12951
    35
lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def 
kleing@12951
    36
                     OutOfMemoryC_def ClassCastC_def
kleing@12951
    37
lemmas class_defs  = list_class_def test_class_def
kleing@12951
    38
kleing@12951
    39
text {* These auxiliary proofs are for efficiency: class lookup,
kleing@12951
    40
subclass relation, method and field lookup are computed only once:
kleing@12951
    41
*}
kleing@12951
    42
lemma class_Object [simp]:
haftmann@28520
    43
  "class E Object = Some (undefined, [],[])"
kleing@12951
    44
  by (simp add: class_def system_defs E_def)
kleing@12951
    45
kleing@12951
    46
lemma class_NullPointer [simp]:
kleing@12951
    47
  "class E (Xcpt NullPointer) = Some (Object, [], [])"
kleing@12951
    48
  by (simp add: class_def system_defs E_def)
kleing@12951
    49
kleing@12951
    50
lemma class_OutOfMemory [simp]:
kleing@12951
    51
  "class E (Xcpt OutOfMemory) = Some (Object, [], [])"
kleing@12951
    52
  by (simp add: class_def system_defs E_def)
kleing@12951
    53
kleing@12951
    54
lemma class_ClassCast [simp]:
kleing@12951
    55
  "class E (Xcpt ClassCast) = Some (Object, [], [])"
kleing@12951
    56
  by (simp add: class_def system_defs E_def)
kleing@12951
    57
kleing@12951
    58
lemma class_list [simp]:
kleing@12951
    59
  "class E list_name = Some list_class"
kleing@12951
    60
  by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
kleing@12951
    61
 
kleing@12951
    62
lemma class_test [simp]:
kleing@12951
    63
  "class E test_name = Some test_class"
kleing@12951
    64
  by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric])
kleing@12951
    65
kleing@12951
    66
lemma E_classes [simp]:
kleing@12951
    67
  "{C. is_class E C} = {list_name, test_name, Xcpt NullPointer, 
kleing@12951
    68
                        Xcpt ClassCast, Xcpt OutOfMemory, Object}"
kleing@12951
    69
  by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs)
kleing@12951
    70
kleing@12951
    71
text {* The subclass releation spelled out: *}
kleing@12951
    72
lemma subcls1:
haftmann@33954
    73
  "subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object),
haftmann@33954
    74
                (Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}"
nipkow@31197
    75
apply (simp add: subcls1_def2)
nipkow@31166
    76
apply (simp add: name_defs class_defs system_defs E_def class_def)
haftmann@33954
    77
apply (simp add: Sigma_def)
haftmann@33954
    78
apply auto
nipkow@31166
    79
done
kleing@12951
    80
kleing@12951
    81
text {* The subclass relation is acyclic; hence its converse is well founded: *}
kleing@12951
    82
lemma notin_rtrancl:
haftmann@33954
    83
  "(a, b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a, y) \<notin> r) \<Longrightarrow> False"
haftmann@33954
    84
  by (auto elim: converse_rtranclE)
kleing@12951
    85
haftmann@33954
    86
lemma acyclic_subcls1_E: "acyclic (subcls1 E)"
haftmann@33954
    87
  apply (rule acyclicI)
kleing@12951
    88
  apply (simp add: subcls1)
haftmann@33954
    89
  apply (auto dest!: tranclD)
kleing@12951
    90
  apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes)
kleing@12951
    91
  done
kleing@12951
    92
haftmann@33954
    93
lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)"
haftmann@33954
    94
  apply (rule finite_acyclic_wf_converse)
berghofe@23757
    95
  apply (simp add: subcls1 del: insert_iff)
kleing@12951
    96
  apply (rule acyclic_subcls1_E)
kleing@12951
    97
  done  
kleing@12951
    98
kleing@12951
    99
text {* Method and field lookup: *}
kleing@12951
   100
lemma method_Object [simp]:
haftmann@31852
   101
  "method (E, Object) = Map.empty"
kleing@12951
   102
  by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
kleing@12951
   103
kleing@12951
   104
lemma method_append [simp]:
kleing@12951
   105
  "method (E, list_name) (append_name, [Class list_name]) =
kleing@12951
   106
  Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])"
kleing@12951
   107
  apply (insert class_list)
kleing@12951
   108
  apply (unfold list_class_def)
kleing@12951
   109
  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   110
  apply simp
kleing@12951
   111
  done
kleing@12951
   112
kleing@12951
   113
lemma method_makelist [simp]:
kleing@12951
   114
  "method (E, test_name) (makelist_name, []) = 
kleing@12951
   115
  Some (test_name, PrimT Void, 3, 2, make_list_ins, [])"
kleing@12951
   116
  apply (insert class_test)
kleing@12951
   117
  apply (unfold test_class_def)
kleing@12951
   118
  apply (drule method_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   119
  apply simp
kleing@12951
   120
  done
kleing@12951
   121
kleing@12951
   122
lemma field_val [simp]:
kleing@12951
   123
  "field (E, list_name) val_name = Some (list_name, PrimT Integer)"
haftmann@23022
   124
  apply (unfold TypeRel.field_def)
kleing@12951
   125
  apply (insert class_list)
kleing@12951
   126
  apply (unfold list_class_def)
kleing@12951
   127
  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   128
  apply simp
kleing@12951
   129
  done
kleing@12951
   130
kleing@12951
   131
lemma field_next [simp]:
kleing@12951
   132
  "field (E, list_name) next_name = Some (list_name, Class list_name)"
haftmann@23022
   133
  apply (unfold TypeRel.field_def)
kleing@12951
   134
  apply (insert class_list)
kleing@12951
   135
  apply (unfold list_class_def)
kleing@12951
   136
  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   137
  apply (simp add: name_defs distinct_fields [symmetric])
kleing@12951
   138
  done
kleing@12951
   139
kleing@12951
   140
lemma [simp]: "fields (E, Object) = []"
kleing@12951
   141
   by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E])
kleing@12951
   142
 
kleing@12951
   143
lemma [simp]: "fields (E, Xcpt NullPointer) = []"
kleing@12951
   144
  by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E])
kleing@12951
   145
kleing@12951
   146
lemma [simp]: "fields (E, Xcpt ClassCast) = []"
kleing@12951
   147
  by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E])
kleing@12951
   148
kleing@12951
   149
lemma [simp]: "fields (E, Xcpt OutOfMemory) = []"
kleing@12951
   150
  by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E])
kleing@12951
   151
kleing@12951
   152
lemma [simp]: "fields (E, test_name) = []"
kleing@12951
   153
  apply (insert class_test)
kleing@12951
   154
  apply (unfold test_class_def)
kleing@12951
   155
  apply (drule fields_rec_lemma [OF _ wf_subcls1_E])
kleing@12951
   156
  apply simp
kleing@12951
   157
  done
kleing@12951
   158
kleing@12951
   159
lemmas [simp] = is_class_def
kleing@12951
   160
kleing@12951
   161
text {*
kleing@12951
   162
  The next definition and three proof rules implement an algorithm to
kleing@12951
   163
  enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} 
kleing@12951
   164
  transforms a goal of the form
kleing@12951
   165
  @{prop [display] "pc < n \<Longrightarrow> P pc"} 
kleing@12951
   166
  into a series of goals
kleing@12951
   167
  @{prop [display] "P 0"} 
kleing@12951
   168
  @{prop [display] "P (Suc 0)"} 
kleing@12951
   169
kleing@12951
   170
  @{text "\<dots>"}
kleing@12951
   171
kleing@12951
   172
  @{prop [display] "P n"} 
kleing@12951
   173
*}
haftmann@35416
   174
definition intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')") where
kleing@12951
   175
  "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
kleing@12951
   176
kleing@12951
   177
lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
kleing@12951
   178
  by (simp add: intervall_def)
kleing@12951
   179
kleing@12951
   180
lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
kleing@12951
   181
  apply (cases "x=n0")
nipkow@13187
   182
  apply (auto simp add: intervall_def)
kleing@12951
   183
  done
kleing@12951
   184
kleing@12951
   185
lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" 
kleing@12951
   186
  by (unfold intervall_def) arith
kleing@12951
   187
kleing@12951
   188
kleing@12951
   189
section "Program structure"
kleing@12951
   190
kleing@12951
   191
text {*
kleing@12951
   192
  The program is structurally wellformed:
kleing@12951
   193
*}
streckem@14045
   194
kleing@12951
   195
lemma wf_struct:
kleing@12951
   196
  "wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E")
kleing@12951
   197
proof -
kleing@12951
   198
  have "unique E" 
kleing@12951
   199
    by (simp add: system_defs E_def class_defs name_defs distinct_classes)
kleing@12951
   200
  moreover
kleing@12951
   201
  have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def)
kleing@12951
   202
  hence "wf_syscls E" by (rule wf_syscls)
kleing@12951
   203
  moreover
kleing@12951
   204
  have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def)
kleing@12951
   205
  moreover
kleing@12951
   206
  have "wf_cdecl ?mb E NullPointerC" 
kleing@12951
   207
    by (auto elim: notin_rtrancl 
kleing@12951
   208
            simp add: wf_cdecl_def name_defs NullPointerC_def subcls1)
kleing@12951
   209
  moreover
kleing@12951
   210
  have "wf_cdecl ?mb E ClassCastC" 
kleing@12951
   211
    by (auto elim: notin_rtrancl 
kleing@12951
   212
            simp add: wf_cdecl_def name_defs ClassCastC_def subcls1)
kleing@12951
   213
  moreover
kleing@12951
   214
  have "wf_cdecl ?mb E OutOfMemoryC" 
kleing@12951
   215
    by (auto elim: notin_rtrancl 
kleing@12951
   216
            simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1)
kleing@12951
   217
  moreover
kleing@12951
   218
  have "wf_cdecl ?mb E (list_name, list_class)"
kleing@12951
   219
    apply (auto elim!: notin_rtrancl 
kleing@12951
   220
            simp add: wf_cdecl_def wf_fdecl_def list_class_def 
kleing@12951
   221
                      wf_mdecl_def wf_mhead_def subcls1)
kleing@12951
   222
    apply (auto simp add: name_defs distinct_classes distinct_fields)
kleing@12951
   223
    done    
kleing@12951
   224
  moreover
kleing@12951
   225
  have "wf_cdecl ?mb E (test_name, test_class)" 
kleing@12951
   226
    apply (auto elim!: notin_rtrancl 
kleing@12951
   227
            simp add: wf_cdecl_def wf_fdecl_def test_class_def 
kleing@12951
   228
                      wf_mdecl_def wf_mhead_def subcls1)
kleing@12951
   229
    apply (auto simp add: name_defs distinct_classes distinct_fields)
kleing@12951
   230
    done       
kleing@12951
   231
  ultimately
streckem@14045
   232
  show ?thesis 
streckem@14045
   233
    by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def)
kleing@12951
   234
qed
kleing@12951
   235
kleing@12951
   236
section "Welltypings"
kleing@12951
   237
text {*
kleing@12951
   238
  We show welltypings of the methods @{term append_name} in class @{term list_name}, 
kleing@12951
   239
  and @{term makelist_name} in class @{term test_name}:
kleing@12951
   240
*}
kleing@12951
   241
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
kleing@12951
   242
declare appInvoke [simp del]
kleing@12951
   243
haftmann@35416
   244
definition phi_append :: method_type ("\<phi>\<^sub>a") where
kleing@12951
   245
  "\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [ 
kleing@12951
   246
   (                                    [], [Class list_name, Class list_name]),
kleing@12951
   247
   (                     [Class list_name], [Class list_name, Class list_name]),
kleing@12951
   248
   (                     [Class list_name], [Class list_name, Class list_name]),
kleing@12951
   249
   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
kleing@12951
   250
   ([NT, Class list_name, Class list_name], [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
   (                          [PrimT Void], [Class list_name, Class list_name]),
kleing@12951
   254
   (                        [Class Object], [Class list_name, Class list_name]),
kleing@12951
   255
   (                                    [], [Class list_name, Class list_name]),
kleing@12951
   256
   (                     [Class list_name], [Class list_name, Class list_name]),
kleing@12951
   257
   (    [Class list_name, Class list_name], [Class list_name, Class list_name]),
kleing@12951
   258
   (                                    [], [Class list_name, Class list_name]),
kleing@12951
   259
   (                          [PrimT Void], [Class list_name, Class list_name])]"
kleing@12951
   260
kleing@13214
   261
kleing@13214
   262
lemma bounded_append [simp]:
kleing@13214
   263
  "check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]"
kleing@13214
   264
  apply (simp add: check_bounded_def)
nipkow@40077
   265
  apply (simp add: eval_nat_numeral append_ins_def)
kleing@13214
   266
  apply (rule allI, rule impI)
kleing@13214
   267
  apply (elim pc_end pc_next pc_0)
kleing@13214
   268
  apply auto
kleing@13214
   269
  done
kleing@13214
   270
kleing@13214
   271
lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)"
kleing@13214
   272
  apply (auto simp add: check_types_def phi_append_def JVM_states_unfold)
kleing@13214
   273
  apply (unfold list_def)
kleing@13214
   274
  apply auto
kleing@13214
   275
  done
kleing@13214
   276
  
kleing@12951
   277
lemma wt_append [simp]:
kleing@12951
   278
  "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins
kleing@12951
   279
             [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a"
kleing@13214
   280
  apply (simp add: wt_method_def wt_start_def wt_instr_def)
kleing@13214
   281
  apply (simp add: phi_append_def append_ins_def)
kleing@12951
   282
  apply clarify
kleing@12951
   283
  apply (elim pc_end pc_next pc_0)
kleing@12951
   284
  apply simp
kleing@12951
   285
  apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1)
kleing@12951
   286
  apply simp
kleing@12951
   287
  apply simp
kleing@12951
   288
  apply (fastsimp simp add: sup_state_conv subcls1)
kleing@12951
   289
  apply simp
kleing@12951
   290
  apply (simp add: app_def xcpt_app_def)
kleing@12951
   291
  apply simp
kleing@12951
   292
  apply simp
kleing@12951
   293
  apply simp
kleing@12951
   294
  apply (simp add: match_exception_entry_def)
kleing@12951
   295
  apply (simp add: match_exception_entry_def)
kleing@12951
   296
  apply simp
kleing@12951
   297
  apply simp
kleing@12951
   298
  done
kleing@12951
   299
kleing@13006
   300
text {* Some abbreviations for readability *} 
wenzelm@35102
   301
abbreviation Clist :: ty 
wenzelm@35102
   302
  where "Clist == Class list_name"
wenzelm@35102
   303
abbreviation Ctest :: ty
wenzelm@35102
   304
  where "Ctest == Class test_name"
kleing@12951
   305
haftmann@35416
   306
definition phi_makelist :: method_type ("\<phi>\<^sub>m") where
kleing@12951
   307
  "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ 
kleing@13214
   308
    (                                   [], [OK Ctest, Err     , Err     ]),
kleing@13214
   309
    (                              [Clist], [OK Ctest, Err     , Err     ]),
kleing@13214
   310
    (                       [Clist, Clist], [OK Ctest, Err     , Err     ]),
kleing@13214
   311
    (                              [Clist], [OK Clist, Err     , Err     ]),
kleing@13214
   312
    (               [PrimT Integer, Clist], [OK Clist, Err     , Err     ]),
kleing@13214
   313
    (                                   [], [OK Clist, Err     , Err     ]),
kleing@13214
   314
    (                              [Clist], [OK Clist, Err     , Err     ]),
kleing@13214
   315
    (                       [Clist, Clist], [OK Clist, Err     , Err     ]),
kleing@13214
   316
    (                              [Clist], [OK Clist, OK Clist, Err     ]),
kleing@13214
   317
    (               [PrimT Integer, Clist], [OK Clist, OK Clist, Err     ]),
kleing@13214
   318
    (                                   [], [OK Clist, OK Clist, Err     ]),
kleing@13214
   319
    (                              [Clist], [OK Clist, OK Clist, Err     ]),
kleing@13214
   320
    (                       [Clist, Clist], [OK Clist, OK Clist, Err     ]),
kleing@13214
   321
    (                              [Clist], [OK Clist, OK Clist, OK Clist]),
kleing@13214
   322
    (               [PrimT Integer, Clist], [OK Clist, OK Clist, OK Clist]),
kleing@13214
   323
    (                                   [], [OK Clist, OK Clist, OK Clist]),
kleing@13214
   324
    (                              [Clist], [OK Clist, OK Clist, OK Clist]),
kleing@13214
   325
    (                       [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
kleing@13214
   326
    (                         [PrimT Void], [OK Clist, OK Clist, OK Clist]),
kleing@13214
   327
    (                                   [], [OK Clist, OK Clist, OK Clist]),
kleing@13214
   328
    (                              [Clist], [OK Clist, OK Clist, OK Clist]),
kleing@13214
   329
    (                       [Clist, Clist], [OK Clist, OK Clist, OK Clist]),
kleing@13214
   330
    (                         [PrimT Void], [OK Clist, OK Clist, OK Clist])]"
kleing@13214
   331
kleing@13214
   332
lemma bounded_makelist [simp]: "check_bounded make_list_ins []"
kleing@13214
   333
  apply (simp add: check_bounded_def)
nipkow@40077
   334
  apply (simp add: eval_nat_numeral make_list_ins_def)
kleing@13214
   335
  apply (rule allI, rule impI)
kleing@13214
   336
  apply (elim pc_end pc_next pc_0)
kleing@13214
   337
  apply auto
kleing@13214
   338
  done
kleing@13214
   339
kleing@13214
   340
lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)"
kleing@13214
   341
  apply (auto simp add: check_types_def phi_makelist_def JVM_states_unfold)
kleing@13214
   342
  apply (unfold list_def)
kleing@13214
   343
  apply auto
kleing@13214
   344
  done
kleing@12951
   345
kleing@12951
   346
lemma wt_makelist [simp]:
kleing@12951
   347
  "wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m"
kleing@13214
   348
  apply (simp add: wt_method_def)
kleing@13214
   349
  apply (simp add: make_list_ins_def phi_makelist_def)
nipkow@40077
   350
  apply (simp add: wt_start_def eval_nat_numeral)
kleing@12951
   351
  apply (simp add: wt_instr_def)
kleing@12951
   352
  apply clarify
kleing@12951
   353
  apply (elim pc_end pc_next pc_0)
kleing@12951
   354
  apply (simp add: match_exception_entry_def)
kleing@12951
   355
  apply simp
kleing@12951
   356
  apply simp
kleing@12951
   357
  apply simp
kleing@12951
   358
  apply (simp add: match_exception_entry_def)
kleing@12951
   359
  apply (simp add: match_exception_entry_def) 
kleing@12951
   360
  apply simp
kleing@12951
   361
  apply simp
kleing@12951
   362
  apply simp
kleing@12951
   363
  apply (simp add: match_exception_entry_def)
kleing@12951
   364
  apply (simp add: match_exception_entry_def) 
kleing@12951
   365
  apply simp
kleing@12951
   366
  apply simp
kleing@12951
   367
  apply simp
kleing@12951
   368
  apply (simp add: match_exception_entry_def)
kleing@12951
   369
  apply (simp add: match_exception_entry_def) 
kleing@12951
   370
  apply simp
kleing@12951
   371
  apply (simp add: app_def xcpt_app_def)
kleing@13101
   372
  apply simp 
kleing@12951
   373
  apply simp
kleing@12951
   374
  apply simp
kleing@13101
   375
  apply (simp add: app_def xcpt_app_def) 
kleing@12951
   376
  apply simp
kleing@12951
   377
  done
kleing@12951
   378
kleing@12951
   379
text {* The whole program is welltyped: *}
haftmann@35416
   380
definition Phi :: prog_type ("\<Phi>") where
kleing@13101
   381
  "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else          
kleing@13101
   382
             if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"
kleing@13139
   383
kleing@12951
   384
lemma wf_prog:
kleing@13101
   385
  "wt_jvm_prog E \<Phi>" 
kleing@12951
   386
  apply (unfold wt_jvm_prog_def)
kleing@12951
   387
  apply (rule wf_mb'E [OF wf_struct])
kleing@12951
   388
  apply (simp add: E_def)
kleing@12951
   389
  apply clarify
kleing@12951
   390
  apply (fold E_def)
kleing@13101
   391
  apply (simp add: system_defs class_defs Phi_def) 
kleing@12951
   392
  apply auto
kleing@13101
   393
  done 
kleing@12951
   394
kleing@12951
   395
kleing@12951
   396
section "Conformance"
kleing@12951
   397
text {* Execution of the program will be typesafe, because its
kleing@12951
   398
  start state conforms to the welltyping: *}
kleing@12951
   399
kleing@13052
   400
lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>"
kleing@13052
   401
  apply (rule BV_correct_initial)
kleing@13052
   402
    apply (rule wf_prog)
kleing@13052
   403
   apply simp
kleing@13052
   404
  apply simp
kleing@12951
   405
  done
kleing@12951
   406
berghofe@13092
   407
berghofe@13092
   408
section "Example for code generation: inferring method types"
berghofe@13092
   409
haftmann@28520
   410
definition test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 
haftmann@28520
   411
             exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state list" where
haftmann@28520
   412
  "test_kil G C pTs rT mxs mxl et instr =
berghofe@13092
   413
   (let first  = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err));
berghofe@13092
   414
        start  = OK first#(replicate (size instr - 1) (OK None))
berghofe@13092
   415
    in  kiljvm G mxs (1+size pTs+mxl) rT et instr start)"
berghofe@13092
   416
berghofe@13092
   417
lemma [code]:
nipkow@15045
   418
  "unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})"
berghofe@13092
   419
  apply (unfold unstables_def)
berghofe@13092
   420
  apply (rule equalityI)
berghofe@13092
   421
  apply (rule subsetI)
berghofe@13092
   422
  apply (erule CollectE)
berghofe@13092
   423
  apply (erule conjE)
berghofe@13092
   424
  apply (rule UN_I)
berghofe@13092
   425
  apply simp
berghofe@13092
   426
  apply simp
berghofe@13092
   427
  apply (rule subsetI)
berghofe@13092
   428
  apply (erule UN_E)
berghofe@13092
   429
  apply (case_tac "\<not> stable r step ss p")
berghofe@13092
   430
  apply simp+
berghofe@13092
   431
  done
berghofe@13092
   432
haftmann@28520
   433
definition some_elem :: "'a set \<Rightarrow> 'a" where
haftmann@28520
   434
  "some_elem = (%S. SOME x. x : S)"
berghofe@13092
   435
berghofe@13092
   436
consts_code
haftmann@31852
   437
  "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")
berghofe@13092
   438
haftmann@28520
   439
text {* This code setup is just a demonstration and \emph{not} sound! *}
haftmann@28520
   440
haftmann@28520
   441
lemma False
haftmann@28520
   442
proof -
haftmann@28520
   443
  have "some_elem (set [False, True]) = False"
haftmann@28520
   444
    by evaluation
haftmann@28520
   445
  moreover have "some_elem (set [True, False]) = True"
haftmann@28520
   446
    by evaluation
haftmann@28520
   447
  ultimately show False
haftmann@28520
   448
    by (simp add: some_elem_def)
haftmann@28520
   449
qed
haftmann@28520
   450
haftmann@28520
   451
lemma [code]:
haftmann@31867
   452
  "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
haftmann@28520
   453
    (\<lambda>(ss, w).
haftmann@28520
   454
        let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
haftmann@28520
   455
    (ss, w)"
haftmann@37024
   456
  unfolding iter_def More_Set.is_empty_def some_elem_def ..
haftmann@20593
   457
berghofe@13092
   458
lemma JVM_sup_unfold [code]:
berghofe@13092
   459
 "JVMType.sup S m n = lift2 (Opt.sup
berghofe@13092
   460
       (Product.sup (Listn.sup (JType.sup S))
berghofe@13092
   461
         (\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" 
berghofe@13092
   462
  apply (unfold JVMType.sup_def JVMType.sl_def Opt.esl_def Err.sl_def
berghofe@13092
   463
         stk_esl_def reg_sl_def Product.esl_def  
berghofe@13092
   464
         Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) 
berghofe@13092
   465
  by simp
berghofe@13092
   466
haftmann@28520
   467
lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold
berghofe@13092
   468
haftmann@31998
   469
lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp
berghofe@13092
   470
berghofe@17145
   471
code_module BV
berghofe@17145
   472
contains
berghofe@13092
   473
  test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
berghofe@13092
   474
    [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
berghofe@13092
   475
  test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
berghofe@17145
   476
ML BV.test1
berghofe@17145
   477
ML BV.test2
berghofe@13092
   478
kleing@13006
   479
end