src/HOL/MicroJava/J/Example.thy
author haftmann
Tue Nov 24 14:37:23 2009 +0100 (2009-11-24)
changeset 33954 1bc3b688548c
parent 28524 644b62cf678f
child 35102 cc7a0b9f938c
permissions -rwxr-xr-x
backported parts of abstract byte code verifier from AFP/Jinja
kleing@12517
     1
(*  Title:      HOL/MicroJava/J/Example.thy
oheimb@9346
     2
    ID:         $Id$
oheimb@9346
     3
    Author:     David von Oheimb
oheimb@11372
     4
    Copyright   1999 Technische Universitaet Muenchen
oheimb@11070
     5
*)
oheimb@9346
     6
kleing@12911
     7
header {* \isaheader{Example MicroJava Program} *}
oheimb@11070
     8
haftmann@16417
     9
theory Example imports SystemClasses Eval begin
oheimb@11070
    10
oheimb@11070
    11
text {* 
oheimb@11070
    12
The following example MicroJava program includes:
oheimb@9346
    13
 class declarations with inheritance, hiding of fields, and overriding of
oheimb@9346
    14
  methods (with refined result type), 
oheimb@9346
    15
 instance creation, local assignment, sequential composition,
oheimb@9346
    16
 method call with dynamic binding, literal values,
oheimb@11070
    17
 expression statement, local access, type cast, field assignment (in part), 
oheimb@11070
    18
 skip.
oheimb@9346
    19
oheimb@11070
    20
\begin{verbatim}
oheimb@9346
    21
class Base {
oheimb@9346
    22
  boolean vee;
oheimb@9346
    23
  Base foo(Base x) {return x;}
oheimb@9346
    24
}
oheimb@9346
    25
oheimb@10229
    26
class Ext extends Base {
oheimb@9346
    27
  int vee;
oheimb@9346
    28
  Ext foo(Base x) {((Ext)x).vee=1; return null;}
oheimb@9346
    29
}
oheimb@9346
    30
oheimb@9346
    31
class Example {
oheimb@9346
    32
  public static void main (String args[]) {
oheimb@9498
    33
    Base e=new Ext();
oheimb@9498
    34
    e.foo(null);
oheimb@9346
    35
  }
oheimb@9346
    36
}
oheimb@11070
    37
\end{verbatim}
oheimb@11070
    38
*}
oheimb@9346
    39
wenzelm@24783
    40
datatype cnam' = Base' | Ext'
wenzelm@24783
    41
datatype vnam' = vee' | x' | e'
oheimb@9346
    42
oheimb@9346
    43
consts
wenzelm@24783
    44
  cnam' :: "cnam' => cname"
wenzelm@24783
    45
  vnam' :: "vnam' => vnam"
oheimb@9346
    46
wenzelm@24783
    47
-- "@{text cnam'} and @{text vnam'} are intended to be isomorphic 
kleing@12517
    48
    to @{text cnam} and @{text vnam}"
kleing@12517
    49
axioms 
wenzelm@24783
    50
  inj_cnam':  "(cnam' x = cnam' y) = (x = y)"
wenzelm@24783
    51
  inj_vnam':  "(vnam' x = vnam' y) = (x = y)"
oheimb@9346
    52
wenzelm@24783
    53
  surj_cnam': "\<exists>m. n = cnam' m"
wenzelm@24783
    54
  surj_vnam': "\<exists>m. n = vnam' m"
oheimb@9346
    55
wenzelm@24783
    56
declare inj_cnam' [simp] inj_vnam' [simp]
oheimb@9346
    57
oheimb@9346
    58
syntax
oheimb@11026
    59
  Base :: cname
oheimb@11026
    60
  Ext  :: cname
oheimb@11026
    61
  vee  :: vname
oheimb@11026
    62
  x    :: vname
oheimb@11026
    63
  e    :: vname
oheimb@9346
    64
oheimb@9346
    65
translations
wenzelm@24783
    66
  "Base" == "cnam' Base'"
wenzelm@24783
    67
  "Ext"  == "cnam' Ext'"
wenzelm@24783
    68
  "vee"  == "VName (vnam' vee')"
wenzelm@24783
    69
  "x"  == "VName (vnam' x')"
wenzelm@24783
    70
  "e"  == "VName (vnam' e')"
oheimb@9346
    71
oheimb@11026
    72
axioms
oheimb@11026
    73
  Base_not_Object: "Base \<noteq> Object"
oheimb@11026
    74
  Ext_not_Object:  "Ext  \<noteq> Object"
kleing@12951
    75
  Base_not_Xcpt:   "Base \<noteq> Xcpt z"
kleing@12951
    76
  Ext_not_Xcpt:    "Ext  \<noteq> Xcpt z"
kleing@12951
    77
  e_not_This:      "e \<noteq> This"  
oheimb@11026
    78
oheimb@11026
    79
declare Base_not_Object [simp] Ext_not_Object [simp]
kleing@12951
    80
declare Base_not_Xcpt [simp] Ext_not_Xcpt [simp]
streckem@11643
    81
declare e_not_This [simp]
kleing@12951
    82
declare Base_not_Object [symmetric, simp]
kleing@12951
    83
declare Ext_not_Object  [symmetric, simp]
kleing@12951
    84
declare Base_not_Xcpt [symmetric, simp]
kleing@12951
    85
declare Ext_not_Xcpt  [symmetric, simp]
oheimb@9346
    86
oheimb@9346
    87
consts
oheimb@11026
    88
  foo_Base::  java_mb
oheimb@11026
    89
  foo_Ext ::  java_mb
oheimb@11026
    90
  BaseC   :: "java_mb cdecl"
oheimb@11026
    91
  ExtC    :: "java_mb cdecl"
kleing@12517
    92
  test    ::  stmt
kleing@12517
    93
  foo   ::  mname
kleing@12517
    94
  a   ::  loc
oheimb@11026
    95
  b       ::  loc
oheimb@9346
    96
oheimb@9346
    97
defs
oheimb@11026
    98
  foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
oheimb@11026
    99
  BaseC_def:"BaseC == (Base, (Object, 
kleing@12517
   100
           [(vee, PrimT Boolean)], 
kleing@12517
   101
           [((foo,[Class Base]),Class Base,foo_Base)]))"
oheimb@11026
   102
  foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
kleing@12517
   103
               (LAcc x)..vee:=Lit (Intg Numeral1)),
kleing@12517
   104
           Lit Null)"
oheimb@11026
   105
  ExtC_def: "ExtC  == (Ext,  (Base  , 
kleing@12517
   106
           [(vee, PrimT Integer)], 
kleing@12517
   107
           [((foo,[Class Base]),Class Ext,foo_Ext)]))"
oheimb@9346
   108
oheimb@11026
   109
  test_def:"test == Expr(e::=NewC Ext);; 
oheimb@10763
   110
                    Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
oheimb@9346
   111
oheimb@9346
   112
wenzelm@20768
   113
abbreviation
wenzelm@21404
   114
  NP  :: xcpt where
wenzelm@20768
   115
  "NP == NullPointer"
oheimb@9346
   116
wenzelm@21404
   117
abbreviation
wenzelm@21404
   118
  tprg  ::"java_mb prog" where
wenzelm@20768
   119
  "tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
wenzelm@20768
   120
wenzelm@21404
   121
abbreviation
wenzelm@21404
   122
  obj1  :: obj where
wenzelm@20768
   123
  "obj1 == (Ext, empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))"
oheimb@9346
   124
wenzelm@21404
   125
abbreviation "s0 == Norm    (empty, empty)"
wenzelm@21404
   126
abbreviation "s1 == Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
wenzelm@21404
   127
abbreviation "s2 == Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
wenzelm@21404
   128
abbreviation "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
oheimb@11026
   129
wenzelm@24074
   130
lemmas map_of_Cons = map_of.simps(2)
wenzelm@24074
   131
oheimb@11026
   132
lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"
oheimb@11026
   133
apply (simp (no_asm))
oheimb@11026
   134
done
oheimb@11026
   135
lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa"
oheimb@11026
   136
apply (simp (no_asm_simp))
oheimb@11026
   137
done
kleing@12517
   138
declare map_of_Cons [simp del] -- "sic!"
oheimb@11026
   139
haftmann@28524
   140
lemma class_tprg_Object [simp]: "class tprg Object = Some (undefined, [], [])"
oheimb@11026
   141
apply (unfold ObjectC_def class_def)
oheimb@11026
   142
apply (simp (no_asm))
oheimb@11026
   143
done
oheimb@11026
   144
kleing@12951
   145
lemma class_tprg_NP [simp]: "class tprg (Xcpt NP) = Some (Object, [], [])"
kleing@12951
   146
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
kleing@12951
   147
apply (simp (no_asm))
kleing@12951
   148
done
kleing@12951
   149
kleing@12951
   150
lemma class_tprg_OM [simp]: "class tprg (Xcpt OutOfMemory) = Some (Object, [], [])"
kleing@12951
   151
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
kleing@12951
   152
apply (simp (no_asm))
kleing@12951
   153
done
kleing@12951
   154
kleing@12951
   155
lemma class_tprg_CC [simp]: "class tprg (Xcpt ClassCast) = Some (Object, [], [])"
kleing@12951
   156
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
kleing@12951
   157
apply (simp (no_asm))
kleing@12951
   158
done
kleing@12951
   159
oheimb@11026
   160
lemma class_tprg_Base [simp]: 
oheimb@11026
   161
"class tprg Base = Some (Object,  
kleing@12517
   162
    [(vee, PrimT Boolean)],  
oheimb@11026
   163
          [((foo, [Class Base]), Class Base, foo_Base)])"
kleing@12951
   164
apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
oheimb@11026
   165
apply (simp (no_asm))
oheimb@11026
   166
done
oheimb@11026
   167
oheimb@11026
   168
lemma class_tprg_Ext [simp]: 
oheimb@11026
   169
"class tprg Ext = Some (Base,  
kleing@12517
   170
    [(vee, PrimT Integer)],  
oheimb@11026
   171
          [((foo, [Class Base]), Class Ext, foo_Ext)])"
oheimb@11026
   172
apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
oheimb@11026
   173
apply (simp (no_asm))
oheimb@11026
   174
done
oheimb@11026
   175
haftmann@33954
   176
lemma not_Object_subcls [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ ==> R"
haftmann@33954
   177
apply (auto dest!: tranclD subcls1D)
oheimb@11026
   178
done
oheimb@11026
   179
oheimb@11026
   180
lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
haftmann@33954
   181
apply (erule rtrancl_induct)
oheimb@11026
   182
apply  auto
oheimb@11026
   183
apply (drule subcls1D)
oheimb@11026
   184
apply auto
oheimb@11026
   185
done
oheimb@11026
   186
haftmann@33954
   187
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+  ==> R"
haftmann@33954
   188
apply (auto dest!: tranclD subcls1D)
oheimb@11026
   189
done
oheimb@11026
   190
oheimb@11026
   191
lemma class_tprgD: 
kleing@12951
   192
"class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory"
kleing@12951
   193
apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
oheimb@11026
   194
apply (auto split add: split_if_asm simp add: map_of_Cons)
oheimb@11026
   195
done
oheimb@11026
   196
haftmann@33954
   197
lemma not_class_subcls_class [elim!]: "(C, C) \<in> (subcls1 tprg)^+ ==> R"
haftmann@33954
   198
apply (auto dest!: tranclD subcls1D)
oheimb@11026
   199
apply (frule class_tprgD)
oheimb@11026
   200
apply (auto dest!:)
haftmann@33954
   201
apply (drule rtranclD)
oheimb@11026
   202
apply auto
oheimb@11026
   203
done
oheimb@11026
   204
oheimb@11026
   205
lemma unique_classes: "unique tprg"
kleing@12951
   206
apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
oheimb@11026
   207
done
oheimb@11026
   208
haftmann@33954
   209
lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"], standard]
oheimb@11026
   210
oheimb@11026
   211
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
oheimb@11026
   212
apply (rule subcls_direct)
oheimb@11026
   213
apply auto
oheimb@11026
   214
done
oheimb@11026
   215
oheimb@11026
   216
lemma Ext_widen_Base [simp]: "tprg\<turnstile>Class Ext\<preceq> Class Base"
oheimb@11026
   217
apply (rule widen.subcls)
oheimb@11026
   218
apply (simp (no_asm))
oheimb@11026
   219
done
oheimb@11026
   220
oheimb@11026
   221
declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
oheimb@11026
   222
haftmann@33954
   223
lemma acyclic_subcls1': "acyclic (subcls1 tprg)"
haftmann@33954
   224
apply (rule acyclicI)
oheimb@11026
   225
apply safe
oheimb@11026
   226
done
oheimb@11026
   227
haftmann@33954
   228
lemmas wf_subcls1' = acyclic_subcls1' [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]]
oheimb@11026
   229
wenzelm@24783
   230
lemmas fields_rec' = wf_subcls1' [THEN [2] fields_rec_lemma]
oheimb@11026
   231
oheimb@11026
   232
lemma fields_Object [simp]: "fields (tprg, Object) = []"
wenzelm@24783
   233
apply (subst fields_rec')
oheimb@11026
   234
apply   auto
oheimb@11026
   235
done
oheimb@11026
   236
oheimb@11026
   237
declare is_class_def [simp]
oheimb@11026
   238
oheimb@11026
   239
lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"
wenzelm@24783
   240
apply (subst fields_rec')
oheimb@11026
   241
apply   auto
oheimb@11026
   242
done
oheimb@11026
   243
oheimb@11026
   244
lemma fields_Ext [simp]: 
oheimb@11026
   245
  "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)"
oheimb@11026
   246
apply (rule trans)
wenzelm@24783
   247
apply  (rule fields_rec')
oheimb@11026
   248
apply   auto
oheimb@11026
   249
done
oheimb@11026
   250
wenzelm@24783
   251
lemmas method_rec' = wf_subcls1' [THEN [2] method_rec_lemma]
oheimb@11026
   252
oheimb@11026
   253
lemma method_Object [simp]: "method (tprg,Object) = map_of []"
wenzelm@24783
   254
apply (subst method_rec')
oheimb@11026
   255
apply  auto
oheimb@11026
   256
done
oheimb@11026
   257
oheimb@11026
   258
lemma method_Base [simp]: "method (tprg, Base) = map_of  
oheimb@11026
   259
  [((foo, [Class Base]), Base, (Class Base, foo_Base))]"
oheimb@11026
   260
apply (rule trans)
wenzelm@24783
   261
apply  (rule method_rec')
oheimb@11026
   262
apply  auto
oheimb@11026
   263
done
oheimb@11026
   264
oheimb@11026
   265
lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of  
oheimb@11026
   266
  [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"
oheimb@11026
   267
apply (rule trans)
wenzelm@24783
   268
apply  (rule method_rec')
oheimb@11026
   269
apply  auto
oheimb@11026
   270
done
oheimb@11026
   271
oheimb@11026
   272
lemma wf_foo_Base: 
oheimb@11026
   273
"wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))"
oheimb@11026
   274
apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Base_def)
oheimb@11026
   275
apply auto
oheimb@11026
   276
done
oheimb@11026
   277
oheimb@11026
   278
lemma wf_foo_Ext: 
oheimb@11026
   279
"wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))"
oheimb@11026
   280
apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Ext_def)
oheimb@11026
   281
apply auto
oheimb@11026
   282
apply  (rule ty_expr_ty_exprs_wt_stmt.Cast)
oheimb@11026
   283
prefer 2
oheimb@11026
   284
apply   (simp)
oheimb@11026
   285
apply   (rule_tac [2] cast.subcls)
oheimb@11026
   286
apply   (unfold field_def)
oheimb@11026
   287
apply   auto
oheimb@11026
   288
done
oheimb@11026
   289
oheimb@11026
   290
lemma wf_ObjectC: 
streckem@14045
   291
"ws_cdecl tprg ObjectC \<and> 
streckem@14045
   292
  wf_cdecl_mdecl wf_java_mdecl tprg ObjectC \<and> wf_mrT tprg ObjectC"
streckem@14045
   293
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
streckem@14045
   294
  wf_mrT_def wf_fdecl_def ObjectC_def)
oheimb@11026
   295
apply (simp (no_asm))
oheimb@11026
   296
done
oheimb@11026
   297
kleing@12951
   298
lemma wf_NP:
streckem@14045
   299
"ws_cdecl tprg NullPointerC \<and>
streckem@14045
   300
  wf_cdecl_mdecl wf_java_mdecl tprg NullPointerC \<and> wf_mrT tprg NullPointerC"
streckem@14045
   301
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
streckem@14045
   302
  wf_mrT_def wf_fdecl_def NullPointerC_def)
kleing@12951
   303
apply (simp add: class_def)
kleing@12951
   304
apply (fold NullPointerC_def class_def)
kleing@12951
   305
apply auto
kleing@12951
   306
done
kleing@12951
   307
kleing@12951
   308
lemma wf_OM:
streckem@14045
   309
"ws_cdecl tprg OutOfMemoryC \<and>
streckem@14045
   310
  wf_cdecl_mdecl wf_java_mdecl tprg OutOfMemoryC \<and> wf_mrT tprg OutOfMemoryC"
streckem@14045
   311
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
streckem@14045
   312
  wf_mrT_def wf_fdecl_def OutOfMemoryC_def)
kleing@12951
   313
apply (simp add: class_def)
kleing@12951
   314
apply (fold OutOfMemoryC_def class_def)
kleing@12951
   315
apply auto
kleing@12951
   316
done
kleing@12951
   317
kleing@12951
   318
lemma wf_CC:
streckem@14045
   319
"ws_cdecl tprg ClassCastC \<and>
streckem@14045
   320
  wf_cdecl_mdecl wf_java_mdecl tprg ClassCastC \<and> wf_mrT tprg ClassCastC"
streckem@14045
   321
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
streckem@14045
   322
  wf_mrT_def wf_fdecl_def ClassCastC_def)
kleing@12951
   323
apply (simp add: class_def)
kleing@12951
   324
apply (fold ClassCastC_def class_def)
kleing@12951
   325
apply auto
kleing@12951
   326
done
kleing@12951
   327
oheimb@11026
   328
lemma wf_BaseC: 
streckem@14045
   329
"ws_cdecl tprg BaseC \<and>
streckem@14045
   330
  wf_cdecl_mdecl wf_java_mdecl tprg BaseC \<and> wf_mrT tprg BaseC"
streckem@14045
   331
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
streckem@14045
   332
  wf_mrT_def wf_fdecl_def BaseC_def)
oheimb@11026
   333
apply (simp (no_asm))
oheimb@11026
   334
apply (fold BaseC_def)
streckem@14045
   335
apply (rule mp) defer apply (rule wf_foo_Base)
streckem@14045
   336
apply (auto simp add: wf_mdecl_def)
streckem@14045
   337
done
streckem@14045
   338
streckem@14045
   339
streckem@14045
   340
lemma wf_ExtC: 
streckem@14045
   341
"ws_cdecl tprg ExtC \<and>
streckem@14045
   342
  wf_cdecl_mdecl wf_java_mdecl tprg ExtC \<and> wf_mrT tprg ExtC"
streckem@14045
   343
apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
streckem@14045
   344
  wf_mrT_def wf_fdecl_def ExtC_def)
streckem@14045
   345
apply (simp (no_asm))
streckem@14045
   346
apply (fold ExtC_def)
streckem@14045
   347
apply (rule mp) defer apply (rule wf_foo_Ext)
streckem@14045
   348
apply (auto simp add: wf_mdecl_def)
haftmann@33954
   349
apply (drule rtranclD)
oheimb@11026
   350
apply auto
oheimb@11026
   351
done
oheimb@11026
   352
oheimb@11026
   353
kleing@12951
   354
lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def)
kleing@12951
   355
oheimb@11026
   356
lemma wf_tprg: 
oheimb@11026
   357
"wf_prog wf_java_mdecl tprg"
streckem@14045
   358
apply (unfold wf_prog_def ws_prog_def Let_def)
kleing@12951
   359
apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes)
kleing@12951
   360
apply (rule wf_syscls)
kleing@12951
   361
apply (simp add: SystemClasses_def)
oheimb@11026
   362
done
oheimb@11026
   363
oheimb@11026
   364
lemma appl_methds_foo_Base: 
oheimb@11026
   365
"appl_methds tprg Base (foo, [NT]) =  
oheimb@11026
   366
  {((Class Base, Class Base), [Class Base])}"
oheimb@11026
   367
apply (unfold appl_methds_def)
oheimb@11026
   368
apply (simp (no_asm))
oheimb@11026
   369
done
oheimb@11026
   370
oheimb@11026
   371
lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) =  
oheimb@11026
   372
  {((Class Base, Class Base), [Class Base])}"
oheimb@11026
   373
apply (unfold max_spec_def)
oheimb@11026
   374
apply (auto simp add: appl_methds_foo_Base)
oheimb@11026
   375
done
oheimb@11026
   376
wenzelm@23894
   377
ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *}
oheimb@11026
   378
lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
oheimb@11026
   379
  Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
kleing@12517
   380
apply (tactic t) -- ";;"
kleing@12517
   381
apply  (tactic t) -- "Expr"
kleing@12517
   382
apply  (tactic t) -- "LAss"
kleing@12517
   383
apply    simp -- {* @{text "e \<noteq> This"} *}
kleing@12517
   384
apply    (tactic t) -- "LAcc"
oheimb@11026
   385
apply     (simp (no_asm))
oheimb@11026
   386
apply    (simp (no_asm))
kleing@12517
   387
apply   (tactic t) -- "NewC"
oheimb@11026
   388
apply   (simp (no_asm))
oheimb@11026
   389
apply  (simp (no_asm))
kleing@12517
   390
apply (tactic t) -- "Expr"
kleing@12517
   391
apply (tactic t) -- "Call"
kleing@12517
   392
apply   (tactic t) -- "LAcc"
oheimb@11026
   393
apply    (simp (no_asm))
oheimb@11026
   394
apply   (simp (no_asm))
kleing@12517
   395
apply  (tactic t) -- "Cons"
kleing@12517
   396
apply   (tactic t) -- "Lit"
oheimb@11026
   397
apply   (simp (no_asm))
kleing@12517
   398
apply  (tactic t) -- "Nil"
oheimb@11026
   399
apply (simp (no_asm))
oheimb@11026
   400
apply (rule max_spec_foo_Base)
oheimb@11026
   401
done
oheimb@11026
   402
wenzelm@23894
   403
ML {* val e = resolve_tac (@{thm NewCI} :: @{thms eval_evals_exec.intros}) 1 *}
oheimb@11026
   404
oheimb@11026
   405
declare split_if [split del]
oheimb@11026
   406
declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
oheimb@11026
   407
lemma exec_test: 
oheimb@11026
   408
" [|new_Addr (heap (snd s0)) = (a, None)|] ==>  
oheimb@11026
   409
  tprg\<turnstile>s0 -test-> ?s"
oheimb@11026
   410
apply (unfold test_def)
kleing@12517
   411
-- "?s = s3 "
kleing@12517
   412
apply (tactic e) -- ";;"
kleing@12517
   413
apply  (tactic e) -- "Expr"
kleing@12517
   414
apply  (tactic e) -- "LAss"
kleing@12517
   415
apply   (tactic e) -- "NewC"
oheimb@11026
   416
apply    force
oheimb@11026
   417
apply   force
oheimb@11026
   418
apply  (simp (no_asm))
oheimb@11026
   419
apply (erule thin_rl)
kleing@12517
   420
apply (tactic e) -- "Expr"
kleing@12517
   421
apply (tactic e) -- "Call"
kleing@12517
   422
apply       (tactic e) -- "LAcc"
oheimb@11026
   423
apply      force
kleing@12517
   424
apply     (tactic e) -- "Cons"
kleing@12517
   425
apply      (tactic e) -- "Lit"
kleing@12517
   426
apply     (tactic e) -- "Nil"
oheimb@11026
   427
apply    (simp (no_asm))
oheimb@11026
   428
apply   (force simp add: foo_Ext_def)
oheimb@11026
   429
apply  (simp (no_asm))
kleing@12517
   430
apply  (tactic e) -- "Expr"
kleing@12517
   431
apply  (tactic e) -- "FAss"
kleing@12517
   432
apply       (tactic e) -- "Cast"
kleing@12517
   433
apply        (tactic e) -- "LAcc"
oheimb@11026
   434
apply       (simp (no_asm))
oheimb@11026
   435
apply      (simp (no_asm))
oheimb@11026
   436
apply     (simp (no_asm))
kleing@12517
   437
apply     (tactic e) -- "XcptE"
oheimb@11026
   438
apply    (simp (no_asm))
oheimb@11026
   439
apply   (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
oheimb@11026
   440
apply  (simp (no_asm))
oheimb@11026
   441
apply (simp (no_asm))
kleing@12517
   442
apply (tactic e) -- "XcptE"
oheimb@11026
   443
done
oheimb@11026
   444
oheimb@9346
   445
end