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