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