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