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