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