src/HOL/Bali/Example.thy
author schirmer
Fri Feb 22 11:26:44 2002 +0100 (2002-02-22)
changeset 12925 99131847fb93
parent 12858 6214f03d6d27
child 13524 604d0f3622d6
permissions -rw-r--r--
Added check for field/method access to operational semantics and proved the acesses valid.
     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_Object [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 Base_foo_member_of_Base: 
   691   "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
   692 by (auto intro!: members.Immediate Base_declares_foo)
   693 
   694 lemma Ext_foo_member_of_Ext: 
   695   "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
   696 by (auto intro!: members.Immediate Ext_declares_foo)
   697 
   698 lemma Ext_foo_member_in_Ext: 
   699   "tprg\<turnstile>(Ext,mdecl Ext_foo) member_in Ext"
   700 by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])
   701 
   702 lemma Base_foo_permits_acc:
   703  "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
   704 by ( simp add: permits_acc_def Base_foo_def)
   705 
   706 lemma Base_foo_accessible [simp]:
   707  "tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S"
   708 by (auto intro: accessible_fromR.Immediate 
   709                 Base_foo_member_of_Base Base_foo_permits_acc)
   710 
   711 lemma Base_foo_dyn_accessible [simp]:
   712  "tprg\<turnstile>(Base,mdecl Base_foo) in Base dyn_accessible_from S"
   713 apply (rule dyn_accessible_fromR.Immediate)
   714 apply   (rule Base_foo_member_in_Base)
   715 apply   (rule Base_foo_permits_acc)
   716 done
   717 
   718 lemma accmethd_Base [simp]: 
   719   "accmethd tprg S Base = methd tprg Base"
   720 apply (simp add: accmethd_def)
   721 apply (rule filter_tab_all_True)
   722 apply (simp add: snd_special_simp fst_special_simp)
   723 done
   724 
   725 lemma Ext_foo_permits_acc:
   726  "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S"
   727 by ( simp add: permits_acc_def Ext_foo_def)
   728 
   729 lemma Ext_foo_accessible [simp]:
   730  "tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S"
   731 by (auto intro: accessible_fromR.Immediate 
   732                 Ext_foo_member_of_Ext Ext_foo_permits_acc)
   733 
   734 lemma Ext_foo_dyn_accessible [simp]:
   735  "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from S"
   736 apply (rule dyn_accessible_fromR.Immediate) 
   737 apply   (rule Ext_foo_member_in_Ext)
   738 apply   (rule Ext_foo_permits_acc)
   739 done
   740 
   741 lemma Ext_foo_overrides_Base_foo:
   742  "tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)"
   743 proof (rule overridesR.Direct, simp_all)
   744   show "\<not> is_static Ext_foo" 
   745     by (simp add: member_is_static_simp Ext_foo_def)
   746   show "\<not> is_static Base_foo"
   747     by (simp add: member_is_static_simp Base_foo_def)
   748   show "accmodi Ext_foo \<noteq> Private"
   749     by (simp add: Ext_foo_def)
   750   show "msig (Ext, Ext_foo) = msig (Base, Base_foo)"
   751     by (simp add: Ext_foo_def Base_foo_def)
   752   show "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
   753     by (auto intro: Ext_declares_foo)
   754   show "tprg\<turnstile>mdecl Base_foo declared_in Base"
   755     by (auto intro: Base_declares_foo)
   756   show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang"
   757     by (simp add: inheritable_in_def Base_foo_def)
   758   show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo"
   759     by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp)
   760 qed
   761 
   762 lemma accmethd_Ext [simp]: 
   763   "accmethd tprg S Ext = methd tprg Ext"
   764 apply (simp add: accmethd_def)
   765 apply (rule filter_tab_all_True)
   766 apply (auto simp add: snd_special_simp fst_special_simp)
   767 done
   768 
   769 lemma cls_Ext: "class tprg Ext = Some ExtCl"
   770 by simp
   771 lemma dynmethd_Ext_foo:
   772  "dynmethd tprg Base Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
   773   = Some (Ext,snd Ext_foo)"
   774 proof -
   775   have "methd tprg Base \<lparr>name = foo, parTs = [Class Base]\<rparr> 
   776           = Some (Base,snd Base_foo)" and
   777        "methd tprg Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
   778           = Some (Ext,snd Ext_foo)" 
   779     by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def)
   780   with cls_Ext ws_tprg Ext_foo_overrides_Base_foo
   781   show ?thesis
   782     by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def)
   783 qed
   784 
   785 lemma Base_fields_accessible[simp]:
   786  "accfield tprg S Base 
   787   = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
   788 apply (auto simp add: accfield_def expand_fun_eq Let_def 
   789                       accessible_in_RefT_simp
   790                       is_public_def
   791                       BaseCl_def
   792                       permits_acc_def
   793                       declared_in_def 
   794                       cdeclaredfield_def
   795                intro!: filter_tab_all_True_Some filter_tab_None
   796                        accessible_fromR.Immediate
   797                intro: members.Immediate)
   798 done
   799 
   800 
   801 lemma arr_member_of_Base:
   802   "tprg\<turnstile>(Base, fdecl (arr, 
   803                  \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
   804           member_of Base"
   805 by (auto intro: members.Immediate 
   806        simp add: declared_in_def cdeclaredfield_def BaseCl_def)
   807  
   808 lemma arr_member_in_Base:
   809   "tprg\<turnstile>(Base, fdecl (arr, 
   810                  \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
   811           member_in Base"
   812 by (rule member_of_to_member_in [OF arr_member_of_Base])
   813 
   814 lemma arr_member_of_Ext:
   815   "tprg\<turnstile>(Base, fdecl (arr, 
   816                     \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
   817              member_of Ext"
   818 apply (rule members.Inherited)
   819 apply   (simp add: inheritable_in_def)
   820 apply   (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def)
   821 apply   (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def)
   822 done
   823 
   824 lemma arr_member_in_Ext:
   825   "tprg\<turnstile>(Base, fdecl (arr, 
   826                  \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
   827           member_in Ext"
   828 by (rule member_of_to_member_in [OF arr_member_of_Ext])
   829 
   830 lemma Ext_fields_accessible[simp]:
   831 "accfield tprg S Ext 
   832   = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
   833 apply (auto simp add: accfield_def expand_fun_eq Let_def 
   834                       accessible_in_RefT_simp
   835                       is_public_def
   836                       BaseCl_def
   837                       ExtCl_def
   838                       permits_acc_def
   839                intro!: filter_tab_all_True_Some filter_tab_None
   840                        accessible_fromR.Immediate)
   841 apply (auto intro: members.Immediate arr_member_of_Ext
   842             simp add: declared_in_def cdeclaredfield_def ExtCl_def)
   843 done
   844 
   845 lemma arr_Base_dyn_accessible [simp]:
   846 "tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
   847        in Base dyn_accessible_from S"
   848 apply (rule dyn_accessible_fromR.Immediate)
   849 apply   (rule arr_member_in_Base)
   850 apply   (simp add: permits_acc_def)
   851 done
   852 
   853 lemma arr_Ext_dyn_accessible[simp]:
   854 "tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
   855        in Ext dyn_accessible_from S"
   856 apply (rule dyn_accessible_fromR.Immediate)
   857 apply   (rule arr_member_in_Ext)
   858 apply   (simp add: permits_acc_def)
   859 done
   860 
   861 lemma array_of_PrimT_acc [simp]:
   862  "is_acc_type tprg java_lang (PrimT t.[])"
   863 apply (simp add: is_acc_type_def accessible_in_RefT_simp)
   864 done
   865 
   866 lemma PrimT_acc [simp]: 
   867  "is_acc_type tprg java_lang (PrimT t)"
   868 apply (simp add: is_acc_type_def accessible_in_RefT_simp)
   869 done
   870 
   871 lemma Object_acc [simp]:
   872  "is_acc_class tprg java_lang Object"
   873 apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def)
   874 done
   875 
   876 
   877 section "well-formedness"
   878 
   879 
   880 lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
   881 apply (unfold wf_idecl_def HasFooInt_def)
   882 apply (auto intro!: wf_mheadI ws_idecl_HasFoo 
   883             simp add: foo_sig_def foo_mhead_def mhead_resTy_simp
   884                       member_is_static_simp )
   885 done
   886 
   887 
   888 declare member_is_static_simp [simp]
   889 declare wt.Skip [rule del] wt.Init [rule del]
   890 lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
   891 lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def
   892 ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
   893 lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
   894 
   895 lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo"
   896 apply (unfold Base_foo_defs )
   897 apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs
   898             simp add: mhead_resTy_simp)
   899 done
   900 
   901 lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo"
   902 apply (unfold Ext_foo_defs )
   903 apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
   904             simp add: mhead_resTy_simp )
   905 apply  (rule wt.Cast)
   906 prefer 2
   907 apply    simp
   908 apply   (rule_tac [2] narrow.subcls [THEN cast.narrow])
   909 apply   (auto intro!: wtIs)
   910 done
   911 
   912 declare mhead_resTy_simp [simp add]
   913 declare member_is_static_simp [simp add]
   914 
   915 lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
   916 apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
   917 apply (auto intro!: wf_Base_foo)
   918 apply       (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
   919 apply (auto intro!: wtIs)
   920 apply (auto simp add: Base_foo_defs entails_def Let_def)
   921 apply   (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+
   922 apply   (insert Base_foo_no_hide         , simp add: Base_foo_def,blast)
   923 done
   924 
   925 
   926 lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
   927 apply (unfold wf_cdecl_def ExtCl_def)
   928 apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
   929 apply (auto simp add: entails_def snd_special_simp)
   930 apply (insert Ext_foo_stat_override)
   931 apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   932 apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   933 apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   934 apply (insert Ext_foo_no_hide)
   935 apply  (simp_all add: qmdecl_def)
   936 apply  blast+
   937 done
   938 
   939 lemma wf_MainC: "wf_cdecl tprg (Main,MainCl)"
   940 apply (unfold wf_cdecl_def MainCl_def)
   941 apply (auto intro: ws_cdecl_Main)
   942 done
   943 
   944 lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)"
   945 apply (simp (no_asm) add: Ifaces_def)
   946 apply (simp (no_asm_simp))
   947 apply (rule wf_HasFoo)
   948 done
   949 
   950 lemma wf_cdecl_all_standard_classes: 
   951   "Ball (set standard_classes) (wf_cdecl tprg)"
   952 apply (unfold standard_classes_def Let_def 
   953        ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
   954 apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
   955 apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def)
   956 apply (auto simp add: Object_def Classes_def standard_classes_def 
   957                       SXcptC_def SXcpt_def)
   958 done
   959 
   960 lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)"
   961 apply (simp (no_asm) add: Classes_def)
   962 apply (simp (no_asm_simp))
   963 apply    (rule wf_BaseC [THEN conjI])
   964 apply   (rule wf_ExtC [THEN conjI])
   965 apply  (rule wf_MainC [THEN conjI])
   966 apply (rule wf_cdecl_all_standard_classes)
   967 done
   968 
   969 theorem wf_tprg: "wf_prog tprg"
   970 apply (unfold wf_prog_def Let_def)
   971 apply (simp (no_asm) add: unique_ifaces unique_classes)
   972 apply (rule conjI)
   973 apply  ((simp (no_asm) add: Classes_def standard_classes_def))
   974 apply (rule conjI)
   975 apply (simp add: Object_mdecls_def)
   976 apply safe
   977 apply  (cut_tac xn_cases_old)   (* FIXME (insert xn_cases) *)
   978 apply  (simp (no_asm_simp) add: Classes_def standard_classes_def)
   979 apply  (insert wf_idecl_all)
   980 apply  (insert wf_cdecl_all)
   981 apply  auto
   982 done
   983 
   984 
   985 section "max spec"
   986 
   987 lemma appl_methds_Base_foo: 
   988 "appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> =  
   989   {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
   990     ,[Class Base])}"
   991 apply (unfold appl_methds_def)
   992 apply (simp (no_asm))
   993 apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
   994 apply  (auto simp add: cmheads_def Base_foo_defs)
   995 done
   996 
   997 lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 
   998   {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
   999    , [Class Base])}"
  1000 apply (unfold max_spec_def)
  1001 apply (simp (no_asm) add: appl_methds_Base_foo)
  1002 apply auto
  1003 done
  1004 
  1005 
  1006 section "well-typedness"
  1007 
  1008 lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
  1009 apply (unfold test_def arr_viewed_from_def)
  1010 (* ?pTs = [Class Base] *)
  1011 apply (rule wtIs (* ;; *))
  1012 apply  (rule wtIs (* Ass *))
  1013 apply  (rule wtIs (* NewC *))
  1014 apply     (rule wtIs (* LVar *))
  1015 apply      (simp)
  1016 apply     (simp)
  1017 apply    (simp)
  1018 apply   (rule wtIs (* NewC *))
  1019 apply   (simp)
  1020 apply  (simp)
  1021 apply (rule wtIs (* Try *))
  1022 prefer 4
  1023 apply    (simp)
  1024 defer
  1025 apply    (rule wtIs (* Expr *))
  1026 apply    (rule wtIs (* Call *))
  1027 apply       (rule wtIs (* Acc *))
  1028 apply       (rule wtIs (* LVar *))
  1029 apply        (simp)
  1030 apply       (simp)
  1031 apply      (rule wtIs (* Cons *))
  1032 apply       (rule wtIs (* Lit *))
  1033 apply       (simp)
  1034 apply      (rule wtIs (* Nil *))
  1035 apply     (simp)
  1036 apply     (rule max_spec_Base_foo)
  1037 apply    (simp)
  1038 apply   (simp)
  1039 apply  (simp)
  1040 apply  (simp)
  1041 apply  (simp)
  1042 apply (rule wtIs (* While *))
  1043 apply  (rule wtIs (* Acc *))
  1044 apply   (rule wtIs (* AVar *))
  1045 apply   (rule wtIs (* Acc *))
  1046 apply   (rule wtIs (* FVar *))
  1047 apply    (rule wtIs (* StatRef *))
  1048 apply    (simp)
  1049 apply   (simp)
  1050 apply   (simp )
  1051 apply   (simp)
  1052 apply   (simp)
  1053 apply  (rule wtIs (* LVar *))
  1054 apply  (simp)
  1055 apply (rule wtIs (* Skip *))
  1056 done
  1057 
  1058 
  1059 section "execution"
  1060 
  1061 lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>  
  1062   new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
  1063 apply (frule atleast_free_SucD)
  1064 apply (drule atleast_free_Suc [THEN iffD1])
  1065 apply clarsimp
  1066 apply (frule new_Addr_SomeI)
  1067 apply force
  1068 done
  1069 
  1070 declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
  1071 declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
  1072 declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
  1073         Base_foo_defs  [simp]
  1074 
  1075 ML {* bind_thms ("eval_intros", map 
  1076         (simplify (simpset() delsimps [thm "Skip_eq"]
  1077                              addsimps [thm "lvar_def"]) o 
  1078          rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
  1079 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
  1080 
  1081 consts
  1082   a :: loc
  1083   b :: loc
  1084   c :: loc
  1085   
  1086 syntax
  1087 
  1088   tprg :: prog
  1089 
  1090   obj_a :: obj
  1091   obj_b :: obj
  1092   obj_c :: obj
  1093   arr_N :: "(vn, val) table"
  1094   arr_a :: "(vn, val) table"
  1095   globs1 :: globs
  1096   globs2 :: globs
  1097   globs3 :: globs
  1098   globs8 :: globs
  1099   locs3 :: locals
  1100   locs4 :: locals
  1101   locs8 :: locals
  1102   s0  :: state
  1103   s0' :: state
  1104   s9' :: state
  1105   s1  :: state
  1106   s1' :: state
  1107   s2  :: state
  1108   s2' :: state
  1109   s3  :: state
  1110   s3' :: state
  1111   s4  :: state
  1112   s4' :: state
  1113   s6' :: state
  1114   s7' :: state
  1115   s8  :: state
  1116   s8' :: state
  1117 
  1118 translations
  1119 
  1120   "tprg"    == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
  1121   
  1122   "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) two
  1123                 ,values=empty(Inr 0\<mapsto>Bool False)(Inr one\<mapsto>Bool False)\<rparr>"
  1124   "obj_b"   <= "\<lparr>tag=CInst Ext
  1125                 ,values=(empty(Inl (vee, Base)\<mapsto>Null   ) 
  1126 			      (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
  1127   "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=empty\<rparr>"
  1128   "arr_N"   == "empty(Inl (arr, Base)\<mapsto>Null)"
  1129   "arr_a"   == "empty(Inl (arr, Base)\<mapsto>Addr a)"
  1130   "globs1"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
  1131 		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
  1132 		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)"
  1133   "globs2"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
  1134 		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
  1135 		     (Inl a\<mapsto>obj_a)
  1136 		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
  1137   "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
  1138   "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
  1139   "locs3"   == "empty(VName e\<mapsto>Addr b)"
  1140   "locs4"   == "empty(VName z\<mapsto>Null)(Inr()\<mapsto>Addr b)"
  1141   "locs8"   == "locs3(VName z\<mapsto>Addr c)"
  1142   "s0"  == "       st empty  empty"
  1143   "s0'" == " Norm  s0"
  1144   "s1"  == "       st globs1 empty"
  1145   "s1'" == " Norm  s1"
  1146   "s2"  == "       st globs2 empty"
  1147   "s2'" == " Norm  s2"
  1148   "s3"  == "       st globs3 locs3 "
  1149   "s3'" == " Norm  s3"
  1150   "s4"  == "       st globs3 locs4"
  1151   "s4'" == " Norm  s4"
  1152   "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
  1153   "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
  1154   "s8"  == "       st globs8 locs8"
  1155   "s8'" == " Norm  s8"
  1156   "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
  1157 
  1158 
  1159 syntax "four"::nat
  1160        "tree"::nat
  1161        "two" ::nat
  1162        "one" ::nat
  1163 translations 
  1164   "one"  == "Suc 0"
  1165   "two"  == "Suc one"
  1166   "tree" == "Suc two"
  1167   "four" == "Suc tree"
  1168 
  1169 declare Pair_eq [simp del]
  1170 lemma exec_test: 
  1171 "\<lbrakk>the (new_Addr (heap  s1)) = a;  
  1172   the (new_Addr (heap ?s2)) = b;  
  1173   the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>  
  1174   atleast_free  (heap s0) four \<Longrightarrow>  
  1175   tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'"
  1176 apply (unfold test_def arr_viewed_from_def)
  1177 (* ?s9' = s9' *)
  1178 apply (simp (no_asm_use))
  1179 apply (drule (1) alloc_one,clarsimp)
  1180 apply (rule eval_Is (* ;; *))
  1181 apply  (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
  1182 apply  (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
  1183 apply  (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
  1184 apply  (rule eval_Is (* Expr *))
  1185 apply  (rule eval_Is (* Ass *))
  1186 apply   (rule eval_Is (* LVar *))
  1187 apply  (rule eval_Is (* NewC *))
  1188       (* begin init Ext *)
  1189 apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
  1190 apply   (erule_tac V = "atleast_free ?h tree" in thin_rl)
  1191 apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
  1192 apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
  1193 apply   (rule eval_Is (* Init Ext *))
  1194 apply   (simp)
  1195 apply   (rule conjI)
  1196 prefer 2 apply (rule conjI HOL.refl)+
  1197 apply   (rule eval_Is (* Init Base *))
  1198 apply   (simp add: arr_viewed_from_def)
  1199 apply   (rule conjI)
  1200 apply    (rule eval_Is (* Init Object *))
  1201 apply    (simp)
  1202 apply    (rule conjI, rule HOL.refl)+
  1203 apply    (rule HOL.refl)
  1204 apply   (simp)
  1205 apply   (rule conjI, rule_tac [2] HOL.refl)
  1206 apply   (rule eval_Is (* Expr *))
  1207 apply   (rule eval_Is (* Ass *))
  1208 apply    (rule eval_Is (* FVar *))
  1209 apply         (rule init_done, simp)
  1210 apply        (rule eval_Is (* StatRef *))
  1211 apply       (simp)
  1212 apply     (simp add: check_field_access_def Let_def) 
  1213 apply   (rule eval_Is (* NewA *))
  1214 apply     (simp)
  1215 apply    (rule eval_Is (* Lit *))
  1216 apply   (simp)
  1217 apply   (rule halloc.New)
  1218 apply    (simp (no_asm_simp))
  1219 apply   (drule atleast_free_weaken,rotate_tac -1,drule atleast_free_weaken)
  1220 apply   (simp (no_asm_simp))
  1221 apply  (simp add: upd_gobj_def)
  1222       (* end init Ext *)
  1223 apply  (rule halloc.New)
  1224 apply   (drule alloc_one)
  1225 prefer 2 apply fast
  1226 apply   (simp (no_asm_simp))
  1227 apply  (drule atleast_free_weaken)
  1228 apply  force
  1229 apply (simp)
  1230 apply (drule alloc_one)
  1231 apply  (simp (no_asm_simp))
  1232 apply clarsimp
  1233 apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
  1234 apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
  1235 apply (simp (no_asm_use))
  1236 apply (rule eval_Is (* Try *))
  1237 apply   (rule eval_Is (* Expr *))
  1238       (* begin method call *)
  1239 apply   (rule eval_Is (* Call *))
  1240 apply      (rule eval_Is (* Acc *))
  1241 apply      (rule eval_Is (* LVar *))
  1242 apply     (rule eval_Is (* Cons *))
  1243 apply      (rule eval_Is (* Lit *))
  1244 apply     (rule eval_Is (* Nil *))
  1245 apply    (simp)
  1246 apply    (simp)
  1247 apply    (subgoal_tac
  1248              "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from Main")
  1249 apply      (simp add: check_method_access_def Let_def
  1250                       invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
  1251 apply      (rule Ext_foo_dyn_accessible)
  1252 apply   (rule eval_Is (* Methd *))
  1253 apply   (simp add: body_def Let_def)
  1254 apply   (rule eval_Is (* Body *))
  1255 apply     (rule init_done, simp)
  1256 apply       (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
  1257 apply    (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
  1258 apply    (rule eval_Is (* Expr *))
  1259 apply    (rule eval_Is (* Ass *))
  1260 apply     (rule eval_Is (* FVar *))
  1261 apply       (rule init_done, simp)
  1262 apply      (rule eval_Is (* Cast *))
  1263 apply       (rule eval_Is (* Acc *))
  1264 apply       (rule eval_Is (* LVar *))
  1265 apply      (simp)
  1266 apply      (simp split del: split_if)
  1267 apply      (simp add: check_field_access_def Let_def)
  1268 apply    (rule eval_Is (* XcptE *))
  1269 apply   (simp)
  1270       (* end method call *)
  1271 apply  (rule sxalloc.intros)
  1272 apply  (rule halloc.New)
  1273 apply   (erule alloc_one [THEN conjunct1])
  1274 apply   (simp (no_asm_simp))
  1275 apply  (simp (no_asm_simp))
  1276 apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
  1277 apply (drule alloc_one [THEN conjunct1])
  1278 apply  (simp (no_asm_simp))
  1279 apply (erule_tac V = "atleast_free ?h two" in thin_rl)
  1280 apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
  1281 apply simp
  1282 apply (rule eval_Is (* While *))
  1283 apply  (rule eval_Is (* Acc *))
  1284 apply  (rule eval_Is (* AVar *))
  1285 apply    (rule eval_Is (* Acc *))
  1286 apply    (rule eval_Is (* FVar *))
  1287 apply      (rule init_done, simp)
  1288 apply     (rule eval_Is (* StatRef *))
  1289 apply    (simp)
  1290 apply    (simp add: check_field_access_def Let_def)
  1291 apply   (rule eval_Is (* Lit *))
  1292 apply  (simp (no_asm_simp))
  1293 apply (auto simp add: in_bounds_def)
  1294 done
  1295 declare Pair_eq [simp]
  1296 
  1297 end