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