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