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