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