src/HOL/Bali/Example.thy
author schirmer
Mon Jan 28 17:00:19 2002 +0100 (2002-01-28)
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
schirmer@12854
     1
(*  Title:      isabelle/Bali/Example.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
schirmer@12854
     4
    Copyright   1997 Technische Universitaet Muenchen
schirmer@12854
     5
*)
schirmer@12854
     6
header {* Example Bali program *}
schirmer@12854
     7
schirmer@12854
     8
theory Example = Eval + WellForm:
schirmer@12854
     9
schirmer@12854
    10
schirmer@12854
    11
text {*
schirmer@12854
    12
The following example Bali program includes:
schirmer@12854
    13
\begin{itemize}
schirmer@12854
    14
\item class and interface declarations with inheritance, hiding of fields,
schirmer@12854
    15
    overriding of methods (with refined result type), array type,
schirmer@12854
    16
\item method call (with dynamic binding), parameter access, return expressions,
schirmer@12854
    17
\item expression statements, sequential composition, literal values, 
schirmer@12854
    18
    local assignment, local access, field assignment, type cast,
schirmer@12854
    19
\item exception generation and propagation, try and catch statement, throw 
schirmer@12854
    20
      statement
schirmer@12854
    21
\item instance creation and (default) static initialization
schirmer@12854
    22
\end{itemize}
schirmer@12854
    23
\begin{verbatim}
schirmer@12854
    24
package java_lang
schirmer@12854
    25
schirmer@12854
    26
public interface HasFoo {
schirmer@12854
    27
  public Base foo(Base z);
schirmer@12854
    28
}
schirmer@12854
    29
schirmer@12854
    30
public class Base implements HasFoo {
schirmer@12854
    31
  static boolean arr[] = new boolean[2];
schirmer@12854
    32
  public HasFoo vee;
schirmer@12854
    33
  public Base foo(Base z) {
schirmer@12854
    34
    return z;
schirmer@12854
    35
  }
schirmer@12854
    36
}
schirmer@12854
    37
schirmer@12854
    38
public class Ext extends Base {
schirmer@12854
    39
  public int vee;
schirmer@12854
    40
  public Ext foo(Base z) {
schirmer@12854
    41
    ((Ext)z).vee = 1;
schirmer@12854
    42
    return null;
schirmer@12854
    43
  }
schirmer@12854
    44
}
schirmer@12854
    45
schirmer@12854
    46
public class Example {
schirmer@12854
    47
  public static void main(String args[]) throws Throwable {
schirmer@12854
    48
    Base e = new Ext();
schirmer@12854
    49
    try {e.foo(null); }
schirmer@12854
    50
    catch(NullPointerException z) { 
schirmer@12854
    51
      while(Ext.arr[2]) ;
schirmer@12854
    52
    }
schirmer@12854
    53
  }
schirmer@12854
    54
}
schirmer@12854
    55
\end{verbatim}
schirmer@12854
    56
*}
schirmer@12854
    57
schirmer@12854
    58
declare widen.null [intro]
schirmer@12854
    59
schirmer@12854
    60
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
schirmer@12854
    61
apply (unfold wf_fdecl_def)
schirmer@12854
    62
apply (simp (no_asm))
schirmer@12854
    63
done
schirmer@12854
    64
schirmer@12854
    65
declare wf_fdecl_def2 [iff]
schirmer@12854
    66
schirmer@12854
    67
schirmer@12854
    68
section "type and expression names"
schirmer@12854
    69
schirmer@12854
    70
(** unfortunately cannot simply instantiate tnam **)
schirmer@12854
    71
datatype tnam_  = HasFoo_ | Base_ | Ext_
schirmer@12854
    72
datatype vnam_  = arr_ | vee_ | z_ | e_
schirmer@12854
    73
datatype label_ = lab1_
schirmer@12854
    74
schirmer@12854
    75
consts
schirmer@12854
    76
schirmer@12854
    77
  tnam_ :: "tnam_  \<Rightarrow> tnam"
schirmer@12854
    78
  vnam_ :: "vnam_  \<Rightarrow> vname"
schirmer@12854
    79
  label_:: "label_ \<Rightarrow> label"
schirmer@12854
    80
axioms  (** tnam_, vnam_ and label are intended to be isomorphic 
schirmer@12854
    81
            to tnam, vname and label **)
schirmer@12854
    82
schirmer@12854
    83
  inj_tnam_  [simp]: "(tnam_  x = tnam_  y) = (x = y)"
schirmer@12854
    84
  inj_vnam_  [simp]: "(vnam_  x = vnam_  y) = (x = y)"
schirmer@12854
    85
  inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
schirmer@12854
    86
  
schirmer@12854
    87
  
schirmer@12854
    88
  surj_tnam_:  "\<exists>m. n = tnam_  m"
schirmer@12854
    89
  surj_vnam_:  "\<exists>m. n = vnam_  m"
schirmer@12854
    90
  surj_label_:" \<exists>m. n = label_ m"
schirmer@12854
    91
schirmer@12854
    92
syntax
schirmer@12854
    93
schirmer@12854
    94
  HasFoo :: qtname
schirmer@12854
    95
  Base   :: qtname
schirmer@12854
    96
  Ext    :: qtname
schirmer@12854
    97
  arr :: ename
schirmer@12854
    98
  vee :: ename
schirmer@12854
    99
  z   :: ename
schirmer@12854
   100
  e   :: ename
schirmer@12854
   101
  lab1:: label
schirmer@12854
   102
translations
schirmer@12854
   103
schirmer@12854
   104
  "HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
schirmer@12854
   105
  "Base"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
schirmer@12854
   106
  "Ext"    == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
schirmer@12854
   107
  "arr"    ==        "(vnam_ arr_)"
schirmer@12854
   108
  "vee"    ==        "(vnam_ vee_)"
schirmer@12854
   109
  "z"      ==        "(vnam_ z_)"
schirmer@12854
   110
  "e"      ==        "(vnam_ e_)"
schirmer@12854
   111
  "lab1"   ==        "label_ lab1_"
schirmer@12854
   112
schirmer@12854
   113
schirmer@12854
   114
lemma neq_Base_Object [simp]: "Base\<noteq>Object"
schirmer@12854
   115
by (simp add: Object_def)
schirmer@12854
   116
schirmer@12854
   117
lemma neq_Ext_Object [simp]: "Ext\<noteq>Object"
schirmer@12854
   118
by (simp add: Object_def)
schirmer@12854
   119
schirmer@12854
   120
lemma neq_Base_SXcpt [simp]: "Base\<noteq>SXcpt xn"
schirmer@12854
   121
by (simp add: SXcpt_def)
schirmer@12854
   122
schirmer@12854
   123
lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
schirmer@12854
   124
by (simp add: SXcpt_def)
schirmer@12854
   125
schirmer@12854
   126
section "classes and interfaces"
schirmer@12854
   127
schirmer@12854
   128
defs
schirmer@12854
   129
schirmer@12854
   130
  Object_mdecls_def: "Object_mdecls \<equiv> []"
schirmer@12854
   131
  SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
schirmer@12854
   132
schirmer@12854
   133
consts
schirmer@12854
   134
  
schirmer@12854
   135
  foo    :: mname
schirmer@12854
   136
schirmer@12854
   137
constdefs
schirmer@12854
   138
  
schirmer@12854
   139
  foo_sig   :: sig
schirmer@12854
   140
 "foo_sig   \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
schirmer@12854
   141
  
schirmer@12854
   142
  foo_mhead :: mhead
schirmer@12854
   143
 "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
schirmer@12854
   144
schirmer@12854
   145
constdefs
schirmer@12854
   146
  
schirmer@12854
   147
  Base_foo :: mdecl
schirmer@12854
   148
 "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
schirmer@12854
   149
                        mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
schirmer@12854
   150
  
schirmer@12854
   151
  Ext_foo  :: mdecl
schirmer@12854
   152
 "Ext_foo  \<equiv> (foo_sig, 
schirmer@12854
   153
              \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
schirmer@12854
   154
	       mbody=\<lparr>lcls=[]
schirmer@12854
   155
                     ,stmt=Expr({Ext,False}Cast (Class Ext) (!!z)..vee := 
schirmer@12854
   156
       	                                                     Lit (Intg 1))\<rparr>
schirmer@12854
   157
	      \<rparr>)"
schirmer@12854
   158
schirmer@12854
   159
constdefs
schirmer@12854
   160
  
schirmer@12854
   161
arr_viewed_from :: "qtname \<Rightarrow> var"
schirmer@12854
   162
"arr_viewed_from C \<equiv> {Base,True}StatRef (ClassT C)..arr"
schirmer@12854
   163
schirmer@12854
   164
BaseCl :: class
schirmer@12854
   165
"BaseCl \<equiv> \<lparr>access=Public,
schirmer@12854
   166
           cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
schirmer@12854
   167
	            (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
schirmer@12854
   168
           methods=[Base_foo],
schirmer@12854
   169
           init=Expr(arr_viewed_from Base :=New (PrimT Boolean)[Lit (Intg 2)]),
schirmer@12854
   170
           super=Object,
schirmer@12854
   171
           superIfs=[HasFoo]\<rparr>"
schirmer@12854
   172
  
schirmer@12854
   173
ExtCl  :: class
schirmer@12854
   174
"ExtCl  \<equiv> \<lparr>access=Public,
schirmer@12854
   175
           cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
schirmer@12854
   176
           methods=[Ext_foo],
schirmer@12854
   177
           init=Skip,
schirmer@12854
   178
           super=Base,
schirmer@12854
   179
           superIfs=[]\<rparr>"
schirmer@12854
   180
schirmer@12854
   181
constdefs
schirmer@12854
   182
  
schirmer@12854
   183
  HasFooInt :: iface
schirmer@12854
   184
 "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
schirmer@12854
   185
schirmer@12854
   186
  Ifaces ::"idecl list"
schirmer@12854
   187
 "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
schirmer@12854
   188
schirmer@12854
   189
 "Classes" ::"cdecl list"
schirmer@12854
   190
 "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl)]@standard_classes"
schirmer@12854
   191
schirmer@12854
   192
lemmas table_classes_defs = 
schirmer@12854
   193
     Classes_def standard_classes_def ObjectC_def SXcptC_def
schirmer@12854
   194
schirmer@12854
   195
lemma table_ifaces [simp]: "table_of Ifaces = empty(HasFoo\<mapsto>HasFooInt)"
schirmer@12854
   196
apply (unfold Ifaces_def)
schirmer@12854
   197
apply (simp (no_asm))
schirmer@12854
   198
done
schirmer@12854
   199
schirmer@12854
   200
lemma table_classes_Object [simp]: 
schirmer@12854
   201
 "table_of Classes Object = Some \<lparr>access=Public,cfields=[]
schirmer@12854
   202
                                 ,methods=Object_mdecls
schirmer@12854
   203
                                 ,init=Skip,super=arbitrary,superIfs=[]\<rparr>"
schirmer@12854
   204
apply (unfold table_classes_defs)
schirmer@12854
   205
apply (simp (no_asm) add:Object_def)
schirmer@12854
   206
done
schirmer@12854
   207
schirmer@12854
   208
lemma table_classes_SXcpt [simp]: 
schirmer@12854
   209
  "table_of Classes (SXcpt xn) 
schirmer@12854
   210
    = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
schirmer@12854
   211
            init=Skip,
schirmer@12854
   212
            super=if xn = Throwable then Object else SXcpt Throwable,
schirmer@12854
   213
            superIfs=[]\<rparr>"
schirmer@12854
   214
apply (unfold table_classes_defs)
schirmer@12854
   215
apply (induct_tac xn)
schirmer@12854
   216
apply (simp add: Object_def SXcpt_def)+
schirmer@12854
   217
done
schirmer@12854
   218
schirmer@12854
   219
lemma table_classes_HasFoo [simp]: "table_of Classes HasFoo = None"
schirmer@12854
   220
apply (unfold table_classes_defs)
schirmer@12854
   221
apply (simp (no_asm) add: Object_def SXcpt_def)
schirmer@12854
   222
done
schirmer@12854
   223
schirmer@12854
   224
lemma table_classes_Base [simp]: "table_of Classes Base = Some BaseCl"
schirmer@12854
   225
apply (unfold table_classes_defs )
schirmer@12854
   226
apply (simp (no_asm) add: Object_def SXcpt_def)
schirmer@12854
   227
done
schirmer@12854
   228
schirmer@12854
   229
lemma table_classes_Ext [simp]: "table_of Classes Ext = Some ExtCl"
schirmer@12854
   230
apply (unfold table_classes_defs )
schirmer@12854
   231
apply (simp (no_asm) add: Object_def SXcpt_def)
schirmer@12854
   232
done
schirmer@12854
   233
schirmer@12854
   234
schirmer@12854
   235
section "program"
schirmer@12854
   236
schirmer@12854
   237
syntax
schirmer@12854
   238
  tprg :: prog
schirmer@12854
   239
schirmer@12854
   240
translations
schirmer@12854
   241
  "tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
schirmer@12854
   242
schirmer@12854
   243
constdefs
schirmer@12854
   244
  test    :: "(ty)list \<Rightarrow> stmt"
schirmer@12854
   245
 "test pTs \<equiv> e:==NewC Ext;; 
schirmer@12854
   246
           \<spacespace> Try Expr({ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
schirmer@12854
   247
           \<spacespace> Catch((SXcpt NullPointer) z)
schirmer@12854
   248
           (lab1\<bullet> While(Acc (Acc (arr_viewed_from Ext).[Lit (Intg 2)])) Skip)"
schirmer@12854
   249
schirmer@12854
   250
schirmer@12854
   251
section "well-structuredness"
schirmer@12854
   252
schirmer@12854
   253
lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
schirmer@12854
   254
apply (auto dest!: tranclD subcls1D)
schirmer@12854
   255
done
schirmer@12854
   256
schirmer@12854
   257
lemma not_Throwable_subcls_SXcpt [elim!]: 
schirmer@12854
   258
  "(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
schirmer@12854
   259
apply (auto dest!: tranclD subcls1D) 
schirmer@12854
   260
apply (simp add: Object_def SXcpt_def)
schirmer@12854
   261
done
schirmer@12854
   262
schirmer@12854
   263
lemma not_SXcpt_n_subcls_SXcpt_n [elim!]: 
schirmer@12854
   264
  "(SXcpt xn, SXcpt xn)  \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
schirmer@12854
   265
apply (auto dest!: tranclD subcls1D)
schirmer@12854
   266
apply (drule rtranclD)
schirmer@12854
   267
apply auto
schirmer@12854
   268
done
schirmer@12854
   269
schirmer@12854
   270
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+  \<Longrightarrow> R"
schirmer@12854
   271
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def)
schirmer@12854
   272
done
schirmer@12854
   273
schirmer@12854
   274
lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]: 
schirmer@12854
   275
  "(\<lparr>pid=java_lang,tid=TName tn\<rparr>, \<lparr>pid=java_lang,tid=TName tn\<rparr>) 
schirmer@12854
   276
   \<in> (subcls1 tprg)^+ \<longrightarrow> R"
schirmer@12854
   277
apply (rule_tac n1 = "tn" in surj_tnam_ [THEN exE])
schirmer@12854
   278
apply (erule ssubst)
schirmer@12854
   279
apply (rule tnam_.induct)
schirmer@12854
   280
apply  safe
schirmer@12854
   281
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def)
schirmer@12854
   282
apply (drule rtranclD)
schirmer@12854
   283
apply auto
schirmer@12854
   284
done
schirmer@12854
   285
schirmer@12854
   286
schirmer@12854
   287
lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []"
schirmer@12854
   288
apply (unfold ws_idecl_def)
schirmer@12854
   289
apply (simp (no_asm))
schirmer@12854
   290
done
schirmer@12854
   291
schirmer@12854
   292
lemma ws_cdecl_Object: "ws_cdecl tprg Object any"
schirmer@12854
   293
apply (unfold ws_cdecl_def)
schirmer@12854
   294
apply auto
schirmer@12854
   295
done
schirmer@12854
   296
schirmer@12854
   297
lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object"
schirmer@12854
   298
apply (unfold ws_cdecl_def)
schirmer@12854
   299
apply auto
schirmer@12854
   300
done
schirmer@12854
   301
schirmer@12854
   302
lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)"
schirmer@12854
   303
apply (unfold ws_cdecl_def)
schirmer@12854
   304
apply auto
schirmer@12854
   305
done
schirmer@12854
   306
schirmer@12854
   307
lemma ws_cdecl_Base: "ws_cdecl tprg Base Object"
schirmer@12854
   308
apply (unfold ws_cdecl_def)
schirmer@12854
   309
apply auto
schirmer@12854
   310
done
schirmer@12854
   311
schirmer@12854
   312
lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base"
schirmer@12854
   313
apply (unfold ws_cdecl_def)
schirmer@12854
   314
apply auto
schirmer@12854
   315
done
schirmer@12854
   316
schirmer@12854
   317
lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable
schirmer@12854
   318
                   ws_cdecl_Base ws_cdecl_Ext
schirmer@12854
   319
schirmer@12854
   320
declare not_Object_subcls_any [rule del]
schirmer@12854
   321
          not_Throwable_subcls_SXcpt [rule del] 
schirmer@12854
   322
          not_SXcpt_n_subcls_SXcpt_n [rule del] 
schirmer@12854
   323
          not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del]
schirmer@12854
   324
schirmer@12854
   325
lemma ws_idecl_all: 
schirmer@12854
   326
 "G=tprg \<Longrightarrow> (\<forall>(I,i)\<in>set Ifaces. ws_idecl G I (isuperIfs i))"
schirmer@12854
   327
apply (simp (no_asm) add: Ifaces_def HasFooInt_def)
schirmer@12854
   328
apply (auto intro!: ws_idecl_HasFoo)
schirmer@12854
   329
done
schirmer@12854
   330
schirmer@12854
   331
lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,c)\<in>set Classes. ws_cdecl G C (super c))"
schirmer@12854
   332
apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def)
schirmer@12854
   333
apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def 
schirmer@12854
   334
        SXcptC_def)
schirmer@12854
   335
done
schirmer@12854
   336
schirmer@12854
   337
lemma ws_tprg: "ws_prog tprg"
schirmer@12854
   338
apply (unfold ws_prog_def)
schirmer@12854
   339
apply (auto intro!: ws_idecl_all ws_cdecl_all)
schirmer@12854
   340
done
schirmer@12854
   341
schirmer@12854
   342
schirmer@12854
   343
section "misc program properties (independent of well-structuredness)"
schirmer@12854
   344
schirmer@12854
   345
lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
schirmer@12854
   346
apply (unfold Ifaces_def)
schirmer@12854
   347
apply (simp (no_asm))
schirmer@12854
   348
done
schirmer@12854
   349
schirmer@12854
   350
lemma empty_subint1 [simp]: "subint1 tprg = {}"
schirmer@12854
   351
apply (unfold subint1_def Ifaces_def HasFooInt_def)
schirmer@12854
   352
apply auto
schirmer@12854
   353
done
schirmer@12854
   354
schirmer@12854
   355
lemma unique_ifaces: "unique Ifaces"
schirmer@12854
   356
apply (unfold Ifaces_def)
schirmer@12854
   357
apply (simp (no_asm))
schirmer@12854
   358
done
schirmer@12854
   359
schirmer@12854
   360
lemma unique_classes: "unique Classes"
schirmer@12854
   361
apply (unfold table_classes_defs )
schirmer@12854
   362
apply (simp )
schirmer@12854
   363
done
schirmer@12854
   364
schirmer@12854
   365
lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
schirmer@12854
   366
apply (rule SXcpt_subcls_Throwable_lemma)
schirmer@12854
   367
apply auto
schirmer@12854
   368
done
schirmer@12854
   369
schirmer@12854
   370
lemma Ext_subclseq_Base [simp]: "tprg\<turnstile>Ext \<preceq>\<^sub>C Base"
schirmer@12854
   371
apply (rule subcls_direct1)
schirmer@12854
   372
apply  (simp (no_asm) add: ExtCl_def)
schirmer@12854
   373
apply  (simp add: Object_def)
schirmer@12854
   374
apply (simp (no_asm))
schirmer@12854
   375
done
schirmer@12854
   376
schirmer@12854
   377
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<prec>\<^sub>C Base"
schirmer@12854
   378
apply (rule subcls_direct2)
schirmer@12854
   379
apply  (simp (no_asm) add: ExtCl_def)
schirmer@12854
   380
apply  (simp add: Object_def)
schirmer@12854
   381
apply (simp (no_asm))
schirmer@12854
   382
done
schirmer@12854
   383
schirmer@12854
   384
schirmer@12854
   385
schirmer@12854
   386
section "fields and method lookup"
schirmer@12854
   387
schirmer@12854
   388
lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []"
schirmer@12854
   389
by (rule ws_tprg [THEN fields_emptyI], force+)
schirmer@12854
   390
schirmer@12854
   391
lemma fields_tprg_Throwable [simp]: 
schirmer@12854
   392
  "DeclConcepts.fields tprg (SXcpt Throwable) = []"
schirmer@12854
   393
by (rule ws_tprg [THEN fields_emptyI], force+)
schirmer@12854
   394
schirmer@12854
   395
lemma fields_tprg_SXcpt [simp]: "DeclConcepts.fields tprg (SXcpt xn) = []"
schirmer@12854
   396
apply (case_tac "xn = Throwable")
schirmer@12854
   397
apply  (simp (no_asm_simp))
schirmer@12854
   398
by (rule ws_tprg [THEN fields_emptyI], force+)
schirmer@12854
   399
schirmer@12854
   400
lemmas fields_rec_ = fields_rec [OF _ ws_tprg]
schirmer@12854
   401
schirmer@12854
   402
lemma fields_Base [simp]: 
schirmer@12854
   403
"DeclConcepts.fields tprg Base 
schirmer@12854
   404
  = [((arr,Base), \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
schirmer@12854
   405
     ((vee,Base), \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)]"
schirmer@12854
   406
apply (subst fields_rec_)
schirmer@12854
   407
apply   (auto simp add: BaseCl_def)
schirmer@12854
   408
done
schirmer@12854
   409
schirmer@12854
   410
lemma fields_Ext [simp]: 
schirmer@12854
   411
 "DeclConcepts.fields tprg Ext  
schirmer@12854
   412
  = [((vee,Ext), \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)] 
schirmer@12854
   413
    @ DeclConcepts.fields tprg Base"
schirmer@12854
   414
apply (rule trans)
schirmer@12854
   415
apply (rule fields_rec_)
schirmer@12854
   416
apply   (auto simp add: ExtCl_def Object_def)
schirmer@12854
   417
done
schirmer@12854
   418
schirmer@12854
   419
lemmas imethds_rec_ = imethds_rec [OF _ ws_tprg]
schirmer@12854
   420
lemmas methd_rec_  = methd_rec  [OF _ ws_tprg]
schirmer@12854
   421
schirmer@12854
   422
lemma imethds_HasFoo [simp]: 
schirmer@12854
   423
  "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
schirmer@12854
   424
apply (rule trans)
schirmer@12854
   425
apply (rule imethds_rec_)
schirmer@12854
   426
apply  (auto simp add: HasFooInt_def)
schirmer@12854
   427
done
schirmer@12854
   428
schirmer@12854
   429
lemma methd_tprg_Object [simp]: "methd tprg Object = empty"
schirmer@12854
   430
apply (subst methd_rec_)
schirmer@12854
   431
apply (auto simp add: Object_mdecls_def)
schirmer@12854
   432
done
schirmer@12854
   433
schirmer@12854
   434
lemma methd_Base [simp]: 
schirmer@12854
   435
  "methd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]"
schirmer@12854
   436
apply (rule trans)
schirmer@12854
   437
apply (rule methd_rec_)
schirmer@12854
   438
apply   (auto simp add: BaseCl_def)
schirmer@12854
   439
done
schirmer@12854
   440
schirmer@12854
   441
(* ### To Table *)
schirmer@12854
   442
lemma filter_tab_all_False: 
schirmer@12854
   443
 "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
schirmer@12854
   444
by (auto simp add: filter_tab_def expand_fun_eq)
schirmer@12854
   445
schirmer@12854
   446
schirmer@12854
   447
lemma memberid_Base_foo_simp [simp]:
schirmer@12854
   448
 "memberid (mdecl Base_foo) = mid foo_sig"
schirmer@12854
   449
by (simp add: Base_foo_def)
schirmer@12854
   450
schirmer@12854
   451
lemma memberid_Ext_foo_simp [simp]:
schirmer@12854
   452
 "memberid (mdecl Ext_foo) = mid foo_sig"
schirmer@12854
   453
by (simp add: Ext_foo_def)
schirmer@12854
   454
schirmer@12854
   455
lemma Base_declares_foo:
schirmer@12854
   456
  "tprg\<turnstile>mdecl Base_foo declared_in Base"
schirmer@12854
   457
by (auto simp add: declared_in_def cdeclaredmethd_def BaseCl_def Base_foo_def)
schirmer@12854
   458
schirmer@12854
   459
lemma foo_sig_not_undeclared_in_Base:
schirmer@12854
   460
  "\<not> tprg\<turnstile>mid foo_sig undeclared_in Base"
schirmer@12854
   461
proof -
schirmer@12854
   462
  from Base_declares_foo
schirmer@12854
   463
  show ?thesis
schirmer@12854
   464
    by (auto dest!: declared_not_undeclared )
schirmer@12854
   465
qed
schirmer@12854
   466
schirmer@12854
   467
lemma Ext_declares_foo:
schirmer@12854
   468
  "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
schirmer@12854
   469
by (auto simp add: declared_in_def cdeclaredmethd_def ExtCl_def Ext_foo_def)
schirmer@12854
   470
schirmer@12854
   471
lemma foo_sig_not_undeclared_in_Ext:
schirmer@12854
   472
  "\<not> tprg\<turnstile>mid foo_sig undeclared_in Ext"
schirmer@12854
   473
proof -
schirmer@12854
   474
  from Ext_declares_foo
schirmer@12854
   475
  show ?thesis
schirmer@12854
   476
    by (auto dest!: declared_not_undeclared )
schirmer@12854
   477
qed
schirmer@12854
   478
schirmer@12854
   479
lemma Base_foo_not_inherited_in_Ext:
schirmer@12854
   480
 "\<not> tprg \<turnstile> Ext inherits (Base,mdecl Base_foo)"
schirmer@12854
   481
by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext)
schirmer@12854
   482
schirmer@12854
   483
lemma Ext_method_inheritance:
schirmer@12854
   484
 "filter_tab (\<lambda>sig m. tprg \<turnstile> Ext inherits method sig m)
schirmer@12854
   485
     (empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto>
schirmer@12854
   486
      snd ((\<lambda>(s, m). (s, Base, m)) Base_foo)))
schirmer@12854
   487
  = empty"
schirmer@12854
   488
proof -
schirmer@12854
   489
  from Base_foo_not_inherited_in_Ext
schirmer@12854
   490
  show ?thesis
schirmer@12854
   491
    by (auto intro: filter_tab_all_False simp add: Base_foo_def)
schirmer@12854
   492
qed
schirmer@12854
   493
schirmer@12854
   494
schirmer@12854
   495
lemma methd_Ext [simp]: "methd tprg Ext =   
schirmer@12854
   496
  table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]"
schirmer@12854
   497
apply (rule trans)
schirmer@12854
   498
apply (rule methd_rec_)
schirmer@12854
   499
apply   (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
schirmer@12854
   500
done
schirmer@12854
   501
schirmer@12854
   502
section "accessibility"
schirmer@12854
   503
schirmer@12854
   504
lemma classesDefined: 
schirmer@12854
   505
 "\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc"
schirmer@12854
   506
apply (auto simp add: Classes_def standard_classes_def 
schirmer@12854
   507
                      BaseCl_def ExtCl_def
schirmer@12854
   508
                      SXcptC_def ObjectC_def) 
schirmer@12854
   509
done
schirmer@12854
   510
schirmer@12854
   511
lemma superclassesBase [simp]: "superclasses tprg Base={Object}"
schirmer@12854
   512
proof -
schirmer@12854
   513
  have ws: "ws_prog tprg" by (rule ws_tprg)
schirmer@12854
   514
  then show ?thesis
schirmer@12854
   515
    by (auto simp add: superclasses_rec  BaseCl_def)
schirmer@12854
   516
qed
schirmer@12854
   517
schirmer@12854
   518
lemma superclassesExt [simp]: "superclasses tprg Ext={Base,Object}"
schirmer@12854
   519
proof -
schirmer@12854
   520
  have ws: "ws_prog tprg" by (rule ws_tprg)
schirmer@12854
   521
  then show ?thesis
schirmer@12854
   522
    by (auto simp add: superclasses_rec  ExtCl_def BaseCl_def)
schirmer@12854
   523
qed
schirmer@12854
   524
schirmer@12854
   525
lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P" 
schirmer@12854
   526
by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def)
schirmer@12854
   527
schirmer@12854
   528
lemma HasFoo_is_acc_iface[simp]: "is_acc_iface tprg P HasFoo"
schirmer@12854
   529
by (simp add: is_acc_iface_def)
schirmer@12854
   530
schirmer@12854
   531
lemma HasFoo_is_acc_type[simp]: "is_acc_type tprg P (Iface HasFoo)"
schirmer@12854
   532
by (simp add: is_acc_type_def)
schirmer@12854
   533
schirmer@12854
   534
lemma Base_accessible[simp]:"tprg\<turnstile>(Class Base) accessible_in P" 
schirmer@12854
   535
by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def)
schirmer@12854
   536
schirmer@12854
   537
lemma Base_is_acc_class[simp]: "is_acc_class tprg P Base"
schirmer@12854
   538
by (simp add: is_acc_class_def)
schirmer@12854
   539
schirmer@12854
   540
lemma Base_is_acc_type[simp]: "is_acc_type tprg P (Class Base)"
schirmer@12854
   541
by (simp add: is_acc_type_def)
schirmer@12854
   542
schirmer@12854
   543
lemma Ext_accessible[simp]:"tprg\<turnstile>(Class Ext) accessible_in P" 
schirmer@12854
   544
by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def)
schirmer@12854
   545
schirmer@12854
   546
lemma Ext_is_acc_class[simp]: "is_acc_class tprg P Ext"
schirmer@12854
   547
by (simp add: is_acc_class_def)
schirmer@12854
   548
schirmer@12854
   549
lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)"
schirmer@12854
   550
by (simp add: is_acc_type_def)
schirmer@12854
   551
schirmer@12854
   552
lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty"
schirmer@12854
   553
apply (unfold accmethd_def)
schirmer@12854
   554
apply (simp)
schirmer@12854
   555
done
schirmer@12854
   556
schirmer@12854
   557
lemma  snd_special_simp: "snd ((\<lambda>(s, m). (s, a, m)) x) = (a,snd x)"
schirmer@12854
   558
by (cases x) (auto)
schirmer@12854
   559
schirmer@12854
   560
lemma  fst_special_simp: "fst ((\<lambda>(s, m). (s, a, m)) x) = fst x"
schirmer@12854
   561
by (cases x) (auto)
schirmer@12854
   562
schirmer@12854
   563
lemma foo_sig_undeclared_in_Object:
schirmer@12854
   564
  "tprg\<turnstile>mid foo_sig undeclared_in Object"
schirmer@12854
   565
by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def)
schirmer@12854
   566
schirmer@12854
   567
(* ### To DeclConcepts *)
schirmer@12854
   568
lemma undeclared_not_declared:
schirmer@12854
   569
 "G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C" 
schirmer@12854
   570
by (cases m) (auto simp add: declared_in_def undeclared_in_def)
schirmer@12854
   571
schirmer@12854
   572
schirmer@12854
   573
lemma unique_sig_Base_foo:
schirmer@12854
   574
 "tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base \<Longrightarrow> sig=foo_sig"
schirmer@12854
   575
by (auto simp add: declared_in_def cdeclaredmethd_def 
schirmer@12854
   576
                   Base_foo_def BaseCl_def)
schirmer@12854
   577
schirmer@12854
   578
lemma Base_foo_no_override:
schirmer@12854
   579
 "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides old \<Longrightarrow> P"
schirmer@12854
   580
apply (drule overrides_commonD)
schirmer@12854
   581
apply (clarsimp)
schirmer@12854
   582
apply (frule subclsEval)
schirmer@12854
   583
apply    (rule ws_tprg)
schirmer@12854
   584
apply    (simp)
schirmer@12854
   585
apply    (rule classesDefined) 
schirmer@12854
   586
apply    assumption+
schirmer@12854
   587
apply (frule unique_sig_Base_foo) 
schirmer@12854
   588
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
schirmer@12854
   589
            dest: unique_sig_Base_foo)
schirmer@12854
   590
done
schirmer@12854
   591
schirmer@12854
   592
lemma Base_foo_no_stat_override:
schirmer@12854
   593
 "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides\<^sub>S old \<Longrightarrow> P"
schirmer@12854
   594
apply (drule stat_overrides_commonD)
schirmer@12854
   595
apply (clarsimp)
schirmer@12854
   596
apply (frule subclsEval)
schirmer@12854
   597
apply    (rule ws_tprg)
schirmer@12854
   598
apply    (simp)
schirmer@12854
   599
apply    (rule classesDefined) 
schirmer@12854
   600
apply    assumption+
schirmer@12854
   601
apply (frule unique_sig_Base_foo) 
schirmer@12854
   602
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
schirmer@12854
   603
            dest: unique_sig_Base_foo)
schirmer@12854
   604
done
schirmer@12854
   605
schirmer@12854
   606
schirmer@12854
   607
lemma Base_foo_no_hide:
schirmer@12854
   608
 "tprg,sig\<turnstile>(Base,(snd Base_foo)) hides old \<Longrightarrow> P"
schirmer@12854
   609
by (auto dest: hidesD simp add: Base_foo_def member_is_static_simp)
schirmer@12854
   610
schirmer@12854
   611
lemma Ext_foo_no_hide:
schirmer@12854
   612
 "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) hides old \<Longrightarrow> P"
schirmer@12854
   613
by (auto dest: hidesD simp add: Ext_foo_def member_is_static_simp)
schirmer@12854
   614
schirmer@12854
   615
lemma unique_sig_Ext_foo:
schirmer@12854
   616
 "tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext \<Longrightarrow> sig=foo_sig"
schirmer@12854
   617
by (auto simp add: declared_in_def cdeclaredmethd_def 
schirmer@12854
   618
                   Ext_foo_def ExtCl_def)
schirmer@12854
   619
schirmer@12854
   620
(* ### To DeclConcepts *)
schirmer@12854
   621
lemma unique_declaration: 
schirmer@12854
   622
 "\<lbrakk>G\<turnstile>m declared_in C;  G\<turnstile>n declared_in C; memberid m = memberid n \<rbrakk> 
schirmer@12854
   623
  \<Longrightarrow> m = n"
schirmer@12854
   624
apply (cases m)
schirmer@12854
   625
apply (cases n,
schirmer@12854
   626
        auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+
schirmer@12854
   627
done
schirmer@12854
   628
schirmer@12854
   629
schirmer@12854
   630
lemma Ext_foo_override:
schirmer@12854
   631
 "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old 
schirmer@12854
   632
  \<Longrightarrow> old = (Base,(snd Base_foo))"
schirmer@12854
   633
apply (drule overrides_commonD)
schirmer@12854
   634
apply (clarsimp)
schirmer@12854
   635
apply (frule subclsEval)
schirmer@12854
   636
apply    (rule ws_tprg)
schirmer@12854
   637
apply    (simp)
schirmer@12854
   638
apply    (rule classesDefined) 
schirmer@12854
   639
apply    assumption+
schirmer@12854
   640
apply (frule unique_sig_Ext_foo) 
schirmer@12854
   641
apply (case_tac "old")
schirmer@12854
   642
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
schirmer@12854
   643
apply (auto simp add: ExtCl_def Ext_foo_def
schirmer@12854
   644
                      BaseCl_def Base_foo_def Object_mdecls_def
schirmer@12854
   645
                      split_paired_all
schirmer@12854
   646
                      member_is_static_simp
schirmer@12854
   647
           dest: declared_not_undeclared unique_declaration)
schirmer@12854
   648
done
schirmer@12854
   649
schirmer@12854
   650
lemma Ext_foo_stat_override:
schirmer@12854
   651
 "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides\<^sub>S old 
schirmer@12854
   652
  \<Longrightarrow> old = (Base,(snd Base_foo))"
schirmer@12854
   653
apply (drule stat_overrides_commonD)
schirmer@12854
   654
apply (clarsimp)
schirmer@12854
   655
apply (frule subclsEval)
schirmer@12854
   656
apply    (rule ws_tprg)
schirmer@12854
   657
apply    (simp)
schirmer@12854
   658
apply    (rule classesDefined) 
schirmer@12854
   659
apply    assumption+
schirmer@12854
   660
apply (frule unique_sig_Ext_foo) 
schirmer@12854
   661
apply (case_tac "old")
schirmer@12854
   662
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
schirmer@12854
   663
apply (auto simp add: ExtCl_def Ext_foo_def
schirmer@12854
   664
                      BaseCl_def Base_foo_def Object_mdecls_def
schirmer@12854
   665
                      split_paired_all
schirmer@12854
   666
                      member_is_static_simp
schirmer@12854
   667
           dest: declared_not_undeclared unique_declaration)
schirmer@12854
   668
done
schirmer@12854
   669
schirmer@12854
   670
(*### weiter hoch *)
schirmer@12854
   671
lemma Base_foo_member_of_Base: 
schirmer@12854
   672
  "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
schirmer@12854
   673
by (auto intro!: members.Immediate Base_declares_foo)
schirmer@12854
   674
schirmer@12854
   675
(*### weiter hoch *)
schirmer@12854
   676
lemma Ext_foo_member_of_Ext: 
schirmer@12854
   677
  "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
schirmer@12854
   678
by (auto intro!: members.Immediate Ext_declares_foo)
schirmer@12854
   679
schirmer@12854
   680
lemma Base_foo_permits_acc:
schirmer@12854
   681
 "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
schirmer@12854
   682
by ( simp add: permits_acc_def Base_foo_def)
schirmer@12854
   683
schirmer@12854
   684
lemma Base_foo_accessible [simp]:
schirmer@12854
   685
 "tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S"
schirmer@12854
   686
by (auto intro: accessible_fromR.immediate 
schirmer@12854
   687
                Base_foo_member_of_Base Base_foo_permits_acc)
schirmer@12854
   688
schirmer@12854
   689
lemma accmethd_Base [simp]: 
schirmer@12854
   690
  "accmethd tprg S Base = methd tprg Base"
schirmer@12854
   691
apply (simp add: accmethd_def)
schirmer@12854
   692
apply (rule filter_tab_all_True)
schirmer@12854
   693
apply (simp add: snd_special_simp fst_special_simp)
schirmer@12854
   694
done
schirmer@12854
   695
schirmer@12854
   696
lemma Ext_foo_permits_acc:
schirmer@12854
   697
 "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S"
schirmer@12854
   698
by ( simp add: permits_acc_def Ext_foo_def)
schirmer@12854
   699
schirmer@12854
   700
lemma Ext_foo_accessible [simp]:
schirmer@12854
   701
 "tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S"
schirmer@12854
   702
by (auto intro: accessible_fromR.immediate 
schirmer@12854
   703
                Ext_foo_member_of_Ext Ext_foo_permits_acc)
schirmer@12854
   704
schirmer@12854
   705
(*
schirmer@12854
   706
lemma Base_foo_accessible_through_inheritance_in_Ext [simp]:
schirmer@12854
   707
 "tprg\<turnstile>(Base,snd Base_foo) accessible_through_inheritance_in Ext"
schirmer@12854
   708
apply (rule accessible_through_inheritance.Direct)
schirmer@12854
   709
apply   simp
schirmer@12854
   710
apply   (simp add: accessible_for_inheritance_in_def Base_foo_def)
schirmer@12854
   711
done
schirmer@12854
   712
*)
schirmer@12854
   713
schirmer@12854
   714
lemma Ext_foo_overrides_Base_foo:
schirmer@12854
   715
 "tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)"
schirmer@12854
   716
proof (rule overridesR.Direct, simp_all)
schirmer@12854
   717
  show "\<not> is_static Ext_foo" 
schirmer@12854
   718
    by (simp add: member_is_static_simp Ext_foo_def)
schirmer@12854
   719
  show "\<not> is_static Base_foo"
schirmer@12854
   720
    by (simp add: member_is_static_simp Base_foo_def)
schirmer@12854
   721
  show "accmodi Ext_foo \<noteq> Private"
schirmer@12854
   722
    by (simp add: Ext_foo_def)
schirmer@12854
   723
  show "msig (Ext, Ext_foo) = msig (Base, Base_foo)"
schirmer@12854
   724
    by (simp add: Ext_foo_def Base_foo_def)
schirmer@12854
   725
  show "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
schirmer@12854
   726
    by (auto intro: Ext_declares_foo)
schirmer@12854
   727
  show "tprg\<turnstile>mdecl Base_foo declared_in Base"
schirmer@12854
   728
    by (auto intro: Base_declares_foo)
schirmer@12854
   729
  show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang"
schirmer@12854
   730
    by (simp add: inheritable_in_def Base_foo_def)
schirmer@12854
   731
  show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo"
schirmer@12854
   732
    by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp)
schirmer@12854
   733
qed
schirmer@12854
   734
schirmer@12854
   735
(*
schirmer@12854
   736
lemma Base_foo_of_Ext_accessible[simp]:
schirmer@12854
   737
 "tprg\<turnstile>(Base, mdecl Base_foo) of Ext accessible_from S"
schirmer@12854
   738
apply (auto intro: accessible_fromR.immediate 
schirmer@12854
   739
                Base_foo_member_of_Base Base_foo_permits_acc)
schirmer@12854
   740
apply (rule accessible_fromR.immediate)
schirmer@12854
   741
apply (rule_tac "old"="(Base,Base_foo)" and  sup="Base" 
schirmer@12854
   742
       in accessible_fromR.overriding)
schirmer@12854
   743
apply (auto intro!: Ext_foo_overrides_Base_foo)
schirmer@12854
   744
apply (auto 
schirmer@12854
   745
apply (insert Ext_foo_overrides_Base_foo)
schirmer@12854
   746
apply (rule accessible_fromR.overriding, simp_all)
schirmer@12854
   747
apply (auto intro!: Ext_foo_overrides_Base_foo)
schirmer@12854
   748
apply (auto intro!: accessible_fromR.overriding
schirmer@12854
   749
             intro:   Ext_foo_overrides_Base_foo)
schirmer@12854
   750
by
schirmer@12854
   751
                Ext_foo_member_of_Ext Ext_foo_permits_acc)
schirmer@12854
   752
apply (auto intro!: accessible 
schirmer@12854
   753
apply (auto simp add: method_accessible_from_def accessible_from_def) 
schirmer@12854
   754
apply (simp add: Base_foo_def)
schirmer@12854
   755
done 
schirmer@12854
   756
*)
schirmer@12854
   757
schirmer@12854
   758
lemma accmethd_Ext [simp]: 
schirmer@12854
   759
  "accmethd tprg S Ext = methd tprg Ext"
schirmer@12854
   760
apply (simp add: accmethd_def)
schirmer@12854
   761
apply (rule filter_tab_all_True)
schirmer@12854
   762
apply (auto simp add: snd_special_simp fst_special_simp)
schirmer@12854
   763
done
schirmer@12854
   764
schirmer@12854
   765
(* ### Weiter hoch *)
schirmer@12854
   766
lemma cls_Ext: "class tprg Ext = Some ExtCl"
schirmer@12854
   767
by simp
schirmer@12854
   768
lemma dynmethd_Ext_foo:
schirmer@12854
   769
 "dynmethd tprg Base Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
schirmer@12854
   770
  = Some (Ext,snd Ext_foo)"
schirmer@12854
   771
proof -
schirmer@12854
   772
  have "methd tprg Base \<lparr>name = foo, parTs = [Class Base]\<rparr> 
schirmer@12854
   773
          = Some (Base,snd Base_foo)" and
schirmer@12854
   774
       "methd tprg Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
schirmer@12854
   775
          = Some (Ext,snd Ext_foo)" 
schirmer@12854
   776
    by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def)
schirmer@12854
   777
  with cls_Ext ws_tprg Ext_foo_overrides_Base_foo
schirmer@12854
   778
  show ?thesis
schirmer@12854
   779
    by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def)
schirmer@12854
   780
qed
schirmer@12854
   781
schirmer@12854
   782
lemma Base_fields_accessible[simp]:
schirmer@12854
   783
 "accfield tprg S Base 
schirmer@12854
   784
  = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
schirmer@12854
   785
apply (auto simp add: accfield_def expand_fun_eq Let_def 
schirmer@12854
   786
                      accessible_in_RefT_simp
schirmer@12854
   787
                      is_public_def
schirmer@12854
   788
                      BaseCl_def
schirmer@12854
   789
                      permits_acc_def
schirmer@12854
   790
                      declared_in_def 
schirmer@12854
   791
                      cdeclaredfield_def
schirmer@12854
   792
               intro!: filter_tab_all_True_Some filter_tab_None
schirmer@12854
   793
                       accessible_fromR.immediate
schirmer@12854
   794
               intro: members.Immediate)
schirmer@12854
   795
done
schirmer@12854
   796
schirmer@12854
   797
schirmer@12854
   798
lemma arr_member_of_Base:
schirmer@12854
   799
  "tprg\<turnstile>(Base, fdecl (arr, 
schirmer@12854
   800
                 \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
schirmer@12854
   801
          member_of Base"
schirmer@12854
   802
by (auto intro: members.Immediate 
schirmer@12854
   803
       simp add: declared_in_def cdeclaredfield_def BaseCl_def)
schirmer@12854
   804
 
schirmer@12854
   805
lemma arr_member_of_Ext:
schirmer@12854
   806
  "tprg\<turnstile>(Base, fdecl (arr, 
schirmer@12854
   807
                    \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
schirmer@12854
   808
             member_of Ext"
schirmer@12854
   809
apply (rule members.Inherited)
schirmer@12854
   810
apply   (simp add: inheritable_in_def)
schirmer@12854
   811
apply   (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def)
schirmer@12854
   812
apply   (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def)
schirmer@12854
   813
done
schirmer@12854
   814
schirmer@12854
   815
lemma Ext_fields_accessible[simp]:
schirmer@12854
   816
"accfield tprg S Ext 
schirmer@12854
   817
  = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
schirmer@12854
   818
apply (auto simp add: accfield_def expand_fun_eq Let_def 
schirmer@12854
   819
                      accessible_in_RefT_simp
schirmer@12854
   820
                      is_public_def
schirmer@12854
   821
                      BaseCl_def
schirmer@12854
   822
                      ExtCl_def
schirmer@12854
   823
                      permits_acc_def
schirmer@12854
   824
               intro!: filter_tab_all_True_Some filter_tab_None
schirmer@12854
   825
                       accessible_fromR.immediate)
schirmer@12854
   826
apply (auto intro: members.Immediate arr_member_of_Ext
schirmer@12854
   827
            simp add: declared_in_def cdeclaredfield_def ExtCl_def)
schirmer@12854
   828
done
schirmer@12854
   829
schirmer@12854
   830
lemma array_of_PrimT_acc [simp]:
schirmer@12854
   831
 "is_acc_type tprg java_lang (PrimT t.[])"
schirmer@12854
   832
apply (simp add: is_acc_type_def accessible_in_RefT_simp)
schirmer@12854
   833
done
schirmer@12854
   834
schirmer@12854
   835
lemma PrimT_acc [simp]: 
schirmer@12854
   836
 "is_acc_type tprg java_lang (PrimT t)"
schirmer@12854
   837
apply (simp add: is_acc_type_def accessible_in_RefT_simp)
schirmer@12854
   838
done
schirmer@12854
   839
schirmer@12854
   840
lemma Object_acc [simp]:
schirmer@12854
   841
 "is_acc_class tprg java_lang Object"
schirmer@12854
   842
apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def)
schirmer@12854
   843
done
schirmer@12854
   844
schirmer@12854
   845
schirmer@12854
   846
section "well-formedness"
schirmer@12854
   847
schirmer@12854
   848
schirmer@12854
   849
lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
schirmer@12854
   850
apply (unfold wf_idecl_def HasFooInt_def)
schirmer@12854
   851
apply (auto intro!: wf_mheadI ws_idecl_HasFoo 
schirmer@12854
   852
            simp add: foo_sig_def foo_mhead_def mhead_resTy_simp
schirmer@12854
   853
                      member_is_static_simp )
schirmer@12854
   854
done
schirmer@12854
   855
schirmer@12854
   856
declare wt.Skip [rule del] wt.Init [rule del]
schirmer@12854
   857
lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
schirmer@12854
   858
lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def
schirmer@12854
   859
ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
schirmer@12854
   860
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
schirmer@12854
   861
schirmer@12854
   862
lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo"
schirmer@12854
   863
apply (unfold Base_foo_defs )
schirmer@12854
   864
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs
schirmer@12854
   865
            simp add: mhead_resTy_simp)
schirmer@12854
   866
done
schirmer@12854
   867
schirmer@12854
   868
lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo"
schirmer@12854
   869
apply (unfold Ext_foo_defs )
schirmer@12854
   870
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
schirmer@12854
   871
            simp add: mhead_resTy_simp )
schirmer@12854
   872
apply  (rule wt.Cast)
schirmer@12854
   873
prefer 2
schirmer@12854
   874
apply    simp
schirmer@12854
   875
apply   (rule_tac [2] narrow.subcls [THEN cast.narrow])
schirmer@12854
   876
apply   (auto intro!: wtIs)
schirmer@12854
   877
done
schirmer@12854
   878
schirmer@12854
   879
declare mhead_resTy_simp [simp add]
schirmer@12854
   880
declare member_is_static_simp [simp add]
schirmer@12854
   881
schirmer@12854
   882
lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
schirmer@12854
   883
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
schirmer@12854
   884
apply (auto intro!: wf_Base_foo)
schirmer@12854
   885
apply       (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
schirmer@12854
   886
apply (auto intro!: wtIs)
schirmer@12854
   887
apply (auto simp add: Base_foo_defs entails_def Let_def)
schirmer@12854
   888
apply   (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+
schirmer@12854
   889
apply   (insert Base_foo_no_hide         , simp add: Base_foo_def,blast)
schirmer@12854
   890
done
schirmer@12854
   891
schirmer@12854
   892
schirmer@12854
   893
lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
schirmer@12854
   894
apply (unfold wf_cdecl_def ExtCl_def)
schirmer@12854
   895
apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
schirmer@12854
   896
apply (auto simp add: entails_def snd_special_simp)
schirmer@12854
   897
apply (insert Ext_foo_stat_override)
schirmer@12854
   898
apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
schirmer@12854
   899
apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
schirmer@12854
   900
apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
schirmer@12854
   901
apply (insert Ext_foo_no_hide)
schirmer@12854
   902
apply  (simp_all add: qmdecl_def)
schirmer@12854
   903
apply  blast+
schirmer@12854
   904
done
schirmer@12854
   905
schirmer@12854
   906
lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)"
schirmer@12854
   907
apply (simp (no_asm) add: Ifaces_def)
schirmer@12854
   908
apply (simp (no_asm_simp))
schirmer@12854
   909
apply (rule wf_HasFoo)
schirmer@12854
   910
done
schirmer@12854
   911
schirmer@12854
   912
lemma wf_cdecl_all_standard_classes: 
schirmer@12854
   913
  "Ball (set standard_classes) (wf_cdecl tprg)"
schirmer@12854
   914
apply (unfold standard_classes_def Let_def 
schirmer@12854
   915
       ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
schirmer@12854
   916
apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
schirmer@12854
   917
apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def)
schirmer@12854
   918
apply (auto simp add: Object_def Classes_def standard_classes_def 
schirmer@12854
   919
                      SXcptC_def SXcpt_def)
schirmer@12854
   920
done
schirmer@12854
   921
schirmer@12854
   922
lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)"
schirmer@12854
   923
apply (simp (no_asm) add: Classes_def)
schirmer@12854
   924
apply (simp (no_asm_simp))
schirmer@12854
   925
apply   (rule wf_BaseC [THEN conjI])
schirmer@12854
   926
apply  (rule wf_ExtC [THEN conjI])
schirmer@12854
   927
apply (rule wf_cdecl_all_standard_classes)
schirmer@12854
   928
done
schirmer@12854
   929
schirmer@12854
   930
theorem wf_tprg: "wf_prog tprg"
schirmer@12854
   931
apply (unfold wf_prog_def Let_def)
schirmer@12854
   932
apply (simp (no_asm) add: unique_ifaces unique_classes)
schirmer@12854
   933
apply (rule conjI)
schirmer@12854
   934
apply  ((simp (no_asm) add: Classes_def standard_classes_def))
schirmer@12854
   935
apply (rule conjI)
schirmer@12854
   936
apply (simp add: Object_mdecls_def)
schirmer@12854
   937
apply safe
schirmer@12854
   938
apply  (cut_tac xn_cases_old)   (* FIXME (insert xn_cases) *)
schirmer@12854
   939
apply  (simp (no_asm_simp) add: Classes_def standard_classes_def)
schirmer@12854
   940
apply  (insert wf_idecl_all)
schirmer@12854
   941
apply  (insert wf_cdecl_all)
schirmer@12854
   942
apply  auto
schirmer@12854
   943
done
schirmer@12854
   944
schirmer@12854
   945
schirmer@12854
   946
section "max spec"
schirmer@12854
   947
schirmer@12854
   948
lemma appl_methds_Base_foo: 
schirmer@12854
   949
"appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> =  
schirmer@12854
   950
  {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
schirmer@12854
   951
    ,[Class Base])}"
schirmer@12854
   952
apply (unfold appl_methds_def)
schirmer@12854
   953
apply (simp (no_asm))
schirmer@12854
   954
apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
schirmer@12854
   955
apply  (auto simp add: cmheads_def Base_foo_defs)
schirmer@12854
   956
done
schirmer@12854
   957
schirmer@12854
   958
lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 
schirmer@12854
   959
  {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
schirmer@12854
   960
   , [Class Base])}"
schirmer@12854
   961
apply (unfold max_spec_def)
schirmer@12854
   962
apply (simp (no_asm) add: appl_methds_Base_foo)
schirmer@12854
   963
apply auto
schirmer@12854
   964
done
schirmer@12854
   965
schirmer@12854
   966
schirmer@12854
   967
section "well-typedness"
schirmer@12854
   968
schirmer@12854
   969
lemma wt_test: "\<lparr>prg=tprg,cls=S,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
schirmer@12854
   970
apply (unfold test_def arr_viewed_from_def)
schirmer@12854
   971
(* ?pTs = [Class Base] *)
schirmer@12854
   972
apply (rule wtIs (* ;; *))
schirmer@12854
   973
apply  (rule wtIs (* Ass *))
schirmer@12854
   974
apply  (rule wtIs (* NewC *))
schirmer@12854
   975
apply     (rule wtIs (* LVar *))
schirmer@12854
   976
apply      (simp)
schirmer@12854
   977
apply     (simp)
schirmer@12854
   978
apply    (simp)
schirmer@12854
   979
apply   (rule wtIs (* NewC *))
schirmer@12854
   980
apply   (simp)
schirmer@12854
   981
apply  (simp)
schirmer@12854
   982
apply (rule wtIs (* Try *))
schirmer@12854
   983
prefer 4
schirmer@12854
   984
apply    (simp)
schirmer@12854
   985
defer
schirmer@12854
   986
apply    (rule wtIs (* Expr *))
schirmer@12854
   987
apply    (rule wtIs (* Call *))
schirmer@12854
   988
apply       (rule wtIs (* Acc *))
schirmer@12854
   989
apply       (rule wtIs (* LVar *))
schirmer@12854
   990
apply        (simp)
schirmer@12854
   991
apply       (simp)
schirmer@12854
   992
apply      (rule wtIs (* Cons *))
schirmer@12854
   993
apply       (rule wtIs (* Lit *))
schirmer@12854
   994
apply       (simp)
schirmer@12854
   995
apply      (rule wtIs (* Nil *))
schirmer@12854
   996
apply     (simp)
schirmer@12854
   997
apply     (rule max_spec_Base_foo)
schirmer@12854
   998
apply    (simp)
schirmer@12854
   999
apply   (simp)
schirmer@12854
  1000
apply  (simp)
schirmer@12854
  1001
apply  (simp)
schirmer@12854
  1002
apply (rule wtIs (* While *))
schirmer@12854
  1003
apply  (rule wtIs (* Acc *))
schirmer@12854
  1004
apply   (rule wtIs (* AVar *))
schirmer@12854
  1005
apply   (rule wtIs (* Acc *))
schirmer@12854
  1006
apply   (rule wtIs (* FVar *))
schirmer@12854
  1007
apply    (rule wtIs (* StatRef *))
schirmer@12854
  1008
apply    (simp)
schirmer@12854
  1009
apply   (simp)
schirmer@12854
  1010
apply   (simp )
schirmer@12854
  1011
apply   (simp)
schirmer@12854
  1012
apply  (rule wtIs (* LVar *))
schirmer@12854
  1013
apply  (simp)
schirmer@12854
  1014
apply (rule wtIs (* Skip *))
schirmer@12854
  1015
done
schirmer@12854
  1016
schirmer@12854
  1017
schirmer@12854
  1018
section "execution"
schirmer@12854
  1019
schirmer@12854
  1020
lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1021
  new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
schirmer@12854
  1022
apply (frule atleast_free_SucD)
schirmer@12854
  1023
apply (drule atleast_free_Suc [THEN iffD1])
schirmer@12854
  1024
apply clarsimp
schirmer@12854
  1025
apply (frule new_Addr_SomeI)
schirmer@12854
  1026
apply force
schirmer@12854
  1027
done
schirmer@12854
  1028
schirmer@12854
  1029
declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
schirmer@12854
  1030
declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
schirmer@12854
  1031
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
schirmer@12854
  1032
        Base_foo_defs  [simp]
schirmer@12854
  1033
schirmer@12854
  1034
ML {* bind_thms ("eval_intros", map 
schirmer@12854
  1035
        (simplify (simpset() delsimps [thm "Skip_eq"]
schirmer@12854
  1036
                             addsimps [thm "lvar_def"]) o 
schirmer@12854
  1037
         rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
schirmer@12854
  1038
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
schirmer@12854
  1039
schirmer@12854
  1040
consts
schirmer@12854
  1041
  a :: loc
schirmer@12854
  1042
  b :: loc
schirmer@12854
  1043
  c :: loc
schirmer@12854
  1044
  
schirmer@12854
  1045
syntax
schirmer@12854
  1046
schirmer@12854
  1047
  tprg :: prog
schirmer@12854
  1048
schirmer@12854
  1049
  obj_a :: obj
schirmer@12854
  1050
  obj_b :: obj
schirmer@12854
  1051
  obj_c :: obj
schirmer@12854
  1052
  arr_N :: "(vn, val) table"
schirmer@12854
  1053
  arr_a :: "(vn, val) table"
schirmer@12854
  1054
  globs1 :: globs
schirmer@12854
  1055
  globs2 :: globs
schirmer@12854
  1056
  globs3 :: globs
schirmer@12854
  1057
  globs8 :: globs
schirmer@12854
  1058
  locs3 :: locals
schirmer@12854
  1059
  locs4 :: locals
schirmer@12854
  1060
  locs8 :: locals
schirmer@12854
  1061
  s0  :: state
schirmer@12854
  1062
  s0' :: state
schirmer@12854
  1063
  s9' :: state
schirmer@12854
  1064
  s1  :: state
schirmer@12854
  1065
  s1' :: state
schirmer@12854
  1066
  s2  :: state
schirmer@12854
  1067
  s2' :: state
schirmer@12854
  1068
  s3  :: state
schirmer@12854
  1069
  s3' :: state
schirmer@12854
  1070
  s4  :: state
schirmer@12854
  1071
  s4' :: state
schirmer@12854
  1072
  s6' :: state
schirmer@12854
  1073
  s7' :: state
schirmer@12854
  1074
  s8  :: state
schirmer@12854
  1075
  s8' :: state
schirmer@12854
  1076
schirmer@12854
  1077
translations
schirmer@12854
  1078
schirmer@12854
  1079
  "tprg"    == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
schirmer@12854
  1080
  
schirmer@12854
  1081
  "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) two
schirmer@12854
  1082
                ,values=empty(Inr 0\<mapsto>Bool False)(Inr one\<mapsto>Bool False)\<rparr>"
schirmer@12854
  1083
  "obj_b"   <= "\<lparr>tag=CInst Ext
schirmer@12854
  1084
                ,values=(empty(Inl (vee, Base)\<mapsto>Null   ) 
schirmer@12854
  1085
			      (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
schirmer@12854
  1086
  "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=empty\<rparr>"
schirmer@12854
  1087
  "arr_N"   == "empty(Inl (arr, Base)\<mapsto>Null)"
schirmer@12854
  1088
  "arr_a"   == "empty(Inl (arr, Base)\<mapsto>Addr a)"
schirmer@12854
  1089
  "globs1"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
schirmer@12854
  1090
		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
schirmer@12854
  1091
		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)"
schirmer@12854
  1092
  "globs2"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
schirmer@12854
  1093
		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
schirmer@12854
  1094
		     (Inl a\<mapsto>obj_a)
schirmer@12854
  1095
		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
schirmer@12854
  1096
  "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
schirmer@12854
  1097
  "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
schirmer@12854
  1098
  "locs3"   == "empty(VName e\<mapsto>Addr b)"
schirmer@12854
  1099
  "locs4"   == "empty(VName z\<mapsto>Null)(Inr()\<mapsto>Addr b)"
schirmer@12854
  1100
  "locs8"   == "locs3(VName z\<mapsto>Addr c)"
schirmer@12854
  1101
  "s0"  == "       st empty  empty"
schirmer@12854
  1102
  "s0'" == " Norm  s0"
schirmer@12854
  1103
  "s1"  == "       st globs1 empty"
schirmer@12854
  1104
  "s1'" == " Norm  s1"
schirmer@12854
  1105
  "s2"  == "       st globs2 empty"
schirmer@12854
  1106
  "s2'" == " Norm  s2"
schirmer@12854
  1107
  "s3"  == "       st globs3 locs3 "
schirmer@12854
  1108
  "s3'" == " Norm  s3"
schirmer@12854
  1109
  "s4"  == "       st globs3 locs4"
schirmer@12854
  1110
  "s4'" == " Norm  s4"
schirmer@12854
  1111
  "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
schirmer@12854
  1112
  "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
schirmer@12854
  1113
  "s8"  == "       st globs8 locs8"
schirmer@12854
  1114
  "s8'" == " Norm  s8"
schirmer@12854
  1115
  "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
schirmer@12854
  1116
schirmer@12854
  1117
schirmer@12854
  1118
syntax "four"::nat
schirmer@12854
  1119
       "tree"::nat
schirmer@12854
  1120
       "two" ::nat
schirmer@12854
  1121
       "one" ::nat
schirmer@12854
  1122
translations 
schirmer@12854
  1123
  "one"  == "Suc 0"
schirmer@12854
  1124
  "two"  == "Suc one"
schirmer@12854
  1125
  "tree" == "Suc two"
schirmer@12854
  1126
  "four" == "Suc tree"
schirmer@12854
  1127
schirmer@12854
  1128
declare Pair_eq [simp del]
schirmer@12854
  1129
lemma exec_test: 
schirmer@12854
  1130
"\<lbrakk>the (new_Addr (heap  s1)) = a;  
schirmer@12854
  1131
  the (new_Addr (heap ?s2)) = b;  
schirmer@12854
  1132
  the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>  
schirmer@12854
  1133
  atleast_free  (heap s0) four \<Longrightarrow>  
schirmer@12854
  1134
  tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'"
schirmer@12854
  1135
apply (unfold test_def arr_viewed_from_def)
schirmer@12854
  1136
(* ?s9' = s9' *)
schirmer@12854
  1137
apply (simp (no_asm_use))
schirmer@12854
  1138
apply (drule (1) alloc_one,clarsimp)
schirmer@12854
  1139
apply (rule eval_Is (* ;; *))
schirmer@12854
  1140
apply  (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
schirmer@12854
  1141
apply  (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
schirmer@12854
  1142
apply  (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
schirmer@12854
  1143
apply  (rule eval_Is (* Expr *))
schirmer@12854
  1144
apply  (rule eval_Is (* Ass *))
schirmer@12854
  1145
apply   (rule eval_Is (* LVar *))
schirmer@12854
  1146
apply  (rule eval_Is (* NewC *))
schirmer@12854
  1147
      (* begin init Ext *)
schirmer@12854
  1148
apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
schirmer@12854
  1149
apply   (erule_tac V = "atleast_free ?h tree" in thin_rl)
schirmer@12854
  1150
apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
schirmer@12854
  1151
apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
schirmer@12854
  1152
apply   (rule eval_Is (* Init Ext *))
schirmer@12854
  1153
apply   (simp)
schirmer@12854
  1154
apply   (rule conjI)
schirmer@12854
  1155
prefer 2 apply (rule conjI HOL.refl)+
schirmer@12854
  1156
apply   (rule eval_Is (* Init Base *))
schirmer@12854
  1157
apply   (simp add: arr_viewed_from_def)
schirmer@12854
  1158
apply   (rule conjI)
schirmer@12854
  1159
apply    (rule eval_Is (* Init Object *))
schirmer@12854
  1160
apply    (simp)
schirmer@12854
  1161
apply    (rule conjI, rule HOL.refl)+
schirmer@12854
  1162
apply    (rule HOL.refl)
schirmer@12854
  1163
apply   (simp)
schirmer@12854
  1164
apply   (rule conjI, rule_tac [2] HOL.refl)
schirmer@12854
  1165
apply   (rule eval_Is (* Expr *))
schirmer@12854
  1166
apply   (rule eval_Is (* Ass *))
schirmer@12854
  1167
apply    (rule eval_Is (* FVar *))
schirmer@12854
  1168
apply      (rule init_done, simp)
schirmer@12854
  1169
apply     (rule eval_Is (* StatRef *))
schirmer@12854
  1170
apply    (simp)
schirmer@12854
  1171
apply   (rule eval_Is (* NewA *))
schirmer@12854
  1172
apply     (simp)
schirmer@12854
  1173
apply    (rule eval_Is (* Lit *))
schirmer@12854
  1174
apply   (simp)
schirmer@12854
  1175
apply   (rule halloc.New)
schirmer@12854
  1176
apply    (simp (no_asm_simp))
schirmer@12854
  1177
apply   (drule atleast_free_weaken,rotate_tac -1,drule atleast_free_weaken)
schirmer@12854
  1178
apply   (simp (no_asm_simp))
schirmer@12854
  1179
apply  (simp add: upd_gobj_def)
schirmer@12854
  1180
      (* end init Ext *)
schirmer@12854
  1181
apply  (rule halloc.New)
schirmer@12854
  1182
apply   (drule alloc_one)
schirmer@12854
  1183
prefer 2 apply fast
schirmer@12854
  1184
apply   (simp (no_asm_simp))
schirmer@12854
  1185
apply  (drule atleast_free_weaken)
schirmer@12854
  1186
apply  force
schirmer@12854
  1187
apply (simp)
schirmer@12854
  1188
apply (drule alloc_one)
schirmer@12854
  1189
apply  (simp (no_asm_simp))
schirmer@12854
  1190
apply clarsimp
schirmer@12854
  1191
apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
schirmer@12854
  1192
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
schirmer@12854
  1193
apply (simp (no_asm_use))
schirmer@12854
  1194
apply (rule eval_Is (* Try *))
schirmer@12854
  1195
apply   (rule eval_Is (* Expr *))
schirmer@12854
  1196
      (* begin method call *)
schirmer@12854
  1197
apply   (rule eval_Is (* Call *))
schirmer@12854
  1198
apply      (rule eval_Is (* Acc *))
schirmer@12854
  1199
apply      (rule eval_Is (* LVar *))
schirmer@12854
  1200
apply     (rule eval_Is (* Cons *))
schirmer@12854
  1201
apply      (rule eval_Is (* Lit *))
schirmer@12854
  1202
apply     (rule eval_Is (* Nil *))
schirmer@12854
  1203
apply    (simp)
schirmer@12854
  1204
apply   (simp)
schirmer@12854
  1205
apply   (rule eval_Is (* Methd *))
schirmer@12854
  1206
apply   (simp add: body_def Let_def)
schirmer@12854
  1207
apply   (rule eval_Is (* Body *))
schirmer@12854
  1208
apply     (rule init_done, simp)
schirmer@12854
  1209
apply       (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
schirmer@12854
  1210
apply    (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
schirmer@12854
  1211
apply    (rule eval_Is (* Expr *))
schirmer@12854
  1212
apply    (rule eval_Is (* Ass *))
schirmer@12854
  1213
apply     (rule eval_Is (* FVar *))
schirmer@12854
  1214
apply       (rule init_done, simp)
schirmer@12854
  1215
apply      (rule eval_Is (* Cast *))
schirmer@12854
  1216
apply       (rule eval_Is (* Acc *))
schirmer@12854
  1217
apply       (rule eval_Is (* LVar *))
schirmer@12854
  1218
apply      (simp)
schirmer@12854
  1219
apply     (simp split del: split_if)
schirmer@12854
  1220
apply    (rule eval_Is (* XcptE *))
schirmer@12854
  1221
apply   (simp)
schirmer@12854
  1222
      (* end method call *)
schirmer@12854
  1223
apply  (rule sxalloc.intros)
schirmer@12854
  1224
apply  (rule halloc.New)
schirmer@12854
  1225
apply   (erule alloc_one [THEN conjunct1])
schirmer@12854
  1226
apply   (simp (no_asm_simp))
schirmer@12854
  1227
apply  (simp (no_asm_simp))
schirmer@12854
  1228
apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
schirmer@12854
  1229
apply (drule alloc_one [THEN conjunct1])
schirmer@12854
  1230
apply  (simp (no_asm_simp))
schirmer@12854
  1231
apply (erule_tac V = "atleast_free ?h two" in thin_rl)
schirmer@12854
  1232
apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
schirmer@12854
  1233
apply simp
schirmer@12854
  1234
apply (rule eval_Is (* While *))
schirmer@12854
  1235
apply  (rule eval_Is (* Acc *))
schirmer@12854
  1236
apply  (rule eval_Is (* AVar *))
schirmer@12854
  1237
apply    (rule eval_Is (* Acc *))
schirmer@12854
  1238
apply    (rule eval_Is (* FVar *))
schirmer@12854
  1239
apply      (rule init_done, simp)
schirmer@12854
  1240
apply     (rule eval_Is (* StatRef *))
schirmer@12854
  1241
apply    (simp)
schirmer@12854
  1242
apply   (rule eval_Is (* Lit *))
schirmer@12854
  1243
apply  (simp (no_asm_simp))
schirmer@12854
  1244
apply (auto simp add: in_bounds_def)
schirmer@12854
  1245
done
schirmer@12854
  1246
declare Pair_eq [simp]
schirmer@12854
  1247
schirmer@12854
  1248
end