src/HOL/Bali/Example.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 39302 d7728f65b353
child 46212 d86ef6b96097
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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 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 section "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 section "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            \<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
   279            \<spacespace> Catch((SXcpt NullPointer) z)
   280            (lab1\<bullet> While(Acc 
   281                         (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip))"
   282 
   283 
   284 section "well-structuredness"
   285 
   286 lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
   287 apply (auto dest!: tranclD subcls1D)
   288 done
   289 
   290 lemma not_Throwable_subcls_SXcpt [elim!]: 
   291   "(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
   292 apply (auto dest!: tranclD subcls1D) 
   293 apply (simp add: Object_def SXcpt_def)
   294 done
   295 
   296 lemma not_SXcpt_n_subcls_SXcpt_n [elim!]: 
   297   "(SXcpt xn, SXcpt xn)  \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
   298 apply (auto dest!: tranclD subcls1D)
   299 apply (drule rtranclD)
   300 apply auto
   301 done
   302 
   303 lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+  \<Longrightarrow> R"
   304 apply (auto dest!: tranclD subcls1D simp add: BaseCl_def)
   305 done
   306 
   307 lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]: 
   308   "(\<lparr>pid=java_lang,tid=TName tn\<rparr>, \<lparr>pid=java_lang,tid=TName tn\<rparr>) 
   309    \<in> (subcls1 tprg)^+ \<longrightarrow> R"
   310 apply (rule_tac n1 = "tn" in surj_tnam' [THEN exE])
   311 apply (erule ssubst)
   312 apply (rule tnam'.induct)
   313 apply  safe
   314 apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def MainCl_def)
   315 apply (drule rtranclD)
   316 apply auto
   317 done
   318 
   319 
   320 lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []"
   321 apply (unfold ws_idecl_def)
   322 apply (simp (no_asm))
   323 done
   324 
   325 lemma ws_cdecl_Object: "ws_cdecl tprg Object any"
   326 apply (unfold ws_cdecl_def)
   327 apply auto
   328 done
   329 
   330 lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object"
   331 apply (unfold ws_cdecl_def)
   332 apply auto
   333 done
   334 
   335 lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)"
   336 apply (unfold ws_cdecl_def)
   337 apply auto
   338 done
   339 
   340 lemma ws_cdecl_Base: "ws_cdecl tprg Base Object"
   341 apply (unfold ws_cdecl_def)
   342 apply auto
   343 done
   344 
   345 lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base"
   346 apply (unfold ws_cdecl_def)
   347 apply auto
   348 done
   349 
   350 lemma ws_cdecl_Main: "ws_cdecl tprg Main Object"
   351 apply (unfold ws_cdecl_def)
   352 apply auto
   353 done
   354 
   355 lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable
   356                    ws_cdecl_Base ws_cdecl_Ext ws_cdecl_Main
   357 
   358 declare not_Object_subcls_any [rule del]
   359           not_Throwable_subcls_SXcpt [rule del] 
   360           not_SXcpt_n_subcls_SXcpt_n [rule del] 
   361           not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del]
   362 
   363 lemma ws_idecl_all: 
   364  "G=tprg \<Longrightarrow> (\<forall>(I,i)\<in>set Ifaces. ws_idecl G I (isuperIfs i))"
   365 apply (simp (no_asm) add: Ifaces_def HasFooInt_def)
   366 apply (auto intro!: ws_idecl_HasFoo)
   367 done
   368 
   369 lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,c)\<in>set Classes. ws_cdecl G C (super c))"
   370 apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def MainCl_def)
   371 apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def 
   372         SXcptC_def)
   373 done
   374 
   375 lemma ws_tprg: "ws_prog tprg"
   376 apply (unfold ws_prog_def)
   377 apply (auto intro!: ws_idecl_all ws_cdecl_all)
   378 done
   379 
   380 
   381 section "misc program properties (independent of well-structuredness)"
   382 
   383 lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
   384 apply (unfold Ifaces_def)
   385 apply (simp (no_asm))
   386 done
   387 
   388 lemma empty_subint1 [simp]: "subint1 tprg = {}"
   389 apply (unfold subint1_def Ifaces_def HasFooInt_def)
   390 apply auto
   391 done
   392 
   393 lemma unique_ifaces: "unique Ifaces"
   394 apply (unfold Ifaces_def)
   395 apply (simp (no_asm))
   396 done
   397 
   398 lemma unique_classes: "unique Classes"
   399 apply (unfold table_classes_defs )
   400 apply (simp )
   401 done
   402 
   403 lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
   404 apply (rule SXcpt_subcls_Throwable_lemma)
   405 apply auto
   406 done
   407 
   408 lemma Ext_subclseq_Base [simp]: "tprg\<turnstile>Ext \<preceq>\<^sub>C Base"
   409 apply (rule subcls_direct1)
   410 apply  (simp (no_asm) add: ExtCl_def)
   411 apply  (simp add: Object_def)
   412 apply (simp (no_asm))
   413 done
   414 
   415 lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<prec>\<^sub>C Base"
   416 apply (rule subcls_direct2)
   417 apply  (simp (no_asm) add: ExtCl_def)
   418 apply  (simp add: Object_def)
   419 apply (simp (no_asm))
   420 done
   421 
   422 
   423 
   424 section "fields and method lookup"
   425 
   426 lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []"
   427 by (rule ws_tprg [THEN fields_emptyI], force+)
   428 
   429 lemma fields_tprg_Throwable [simp]: 
   430   "DeclConcepts.fields tprg (SXcpt Throwable) = []"
   431 by (rule ws_tprg [THEN fields_emptyI], force+)
   432 
   433 lemma fields_tprg_SXcpt [simp]: "DeclConcepts.fields tprg (SXcpt xn) = []"
   434 apply (case_tac "xn = Throwable")
   435 apply  (simp (no_asm_simp))
   436 by (rule ws_tprg [THEN fields_emptyI], force+)
   437 
   438 lemmas fields_rec' = fields_rec [OF _ ws_tprg]
   439 
   440 lemma fields_Base [simp]: 
   441 "DeclConcepts.fields tprg Base 
   442   = [((arr,Base), \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
   443      ((vee,Base), \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)]"
   444 apply (subst fields_rec')
   445 apply   (auto simp add: BaseCl_def)
   446 done
   447 
   448 lemma fields_Ext [simp]: 
   449  "DeclConcepts.fields tprg Ext  
   450   = [((vee,Ext), \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)] 
   451     @ DeclConcepts.fields tprg Base"
   452 apply (rule trans)
   453 apply (rule fields_rec')
   454 apply   (auto simp add: ExtCl_def Object_def)
   455 done
   456 
   457 lemmas imethds_rec' = imethds_rec [OF _ ws_tprg]
   458 lemmas methd_rec'  = methd_rec  [OF _ ws_tprg]
   459 
   460 lemma imethds_HasFoo [simp]: 
   461   "imethds tprg HasFoo = Option.set \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
   462 apply (rule trans)
   463 apply (rule imethds_rec')
   464 apply  (auto simp add: HasFooInt_def)
   465 done
   466 
   467 lemma methd_tprg_Object [simp]: "methd tprg Object = empty"
   468 apply (subst methd_rec')
   469 apply (auto simp add: Object_mdecls_def)
   470 done
   471 
   472 lemma methd_Base [simp]: 
   473   "methd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]"
   474 apply (rule trans)
   475 apply (rule methd_rec')
   476 apply   (auto simp add: BaseCl_def)
   477 done
   478 
   479 lemma memberid_Base_foo_simp [simp]:
   480  "memberid (mdecl Base_foo) = mid foo_sig"
   481 by (simp add: Base_foo_def)
   482 
   483 lemma memberid_Ext_foo_simp [simp]:
   484  "memberid (mdecl Ext_foo) = mid foo_sig"
   485 by (simp add: Ext_foo_def)
   486 
   487 lemma Base_declares_foo:
   488   "tprg\<turnstile>mdecl Base_foo declared_in Base"
   489 by (auto simp add: declared_in_def cdeclaredmethd_def BaseCl_def Base_foo_def)
   490 
   491 lemma foo_sig_not_undeclared_in_Base:
   492   "\<not> tprg\<turnstile>mid foo_sig undeclared_in Base"
   493 proof -
   494   from Base_declares_foo
   495   show ?thesis
   496     by (auto dest!: declared_not_undeclared )
   497 qed
   498 
   499 lemma Ext_declares_foo:
   500   "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
   501 by (auto simp add: declared_in_def cdeclaredmethd_def ExtCl_def Ext_foo_def)
   502 
   503 lemma foo_sig_not_undeclared_in_Ext:
   504   "\<not> tprg\<turnstile>mid foo_sig undeclared_in Ext"
   505 proof -
   506   from Ext_declares_foo
   507   show ?thesis
   508     by (auto dest!: declared_not_undeclared )
   509 qed
   510 
   511 lemma Base_foo_not_inherited_in_Ext:
   512  "\<not> tprg \<turnstile> Ext inherits (Base,mdecl Base_foo)"
   513 by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext)
   514 
   515 lemma Ext_method_inheritance:
   516  "filter_tab (\<lambda>sig m. tprg \<turnstile> Ext inherits method sig m)
   517      (empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto>
   518       snd ((\<lambda>(s, m). (s, Base, m)) Base_foo)))
   519   = empty"
   520 proof -
   521   from Base_foo_not_inherited_in_Ext
   522   show ?thesis
   523     by (auto intro: filter_tab_all_False simp add: Base_foo_def)
   524 qed
   525 
   526 
   527 lemma methd_Ext [simp]: "methd tprg Ext =   
   528   table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]"
   529 apply (rule trans)
   530 apply (rule methd_rec')
   531 apply   (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
   532 done
   533 
   534 section "accessibility"
   535 
   536 lemma classesDefined: 
   537  "\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc"
   538 apply (auto simp add: Classes_def standard_classes_def 
   539                       BaseCl_def ExtCl_def MainCl_def
   540                       SXcptC_def ObjectC_def) 
   541 done
   542 
   543 lemma superclassesBase [simp]: "superclasses tprg Base={Object}"
   544 proof -
   545   have ws: "ws_prog tprg" by (rule ws_tprg)
   546   then show ?thesis
   547     by (auto simp add: superclasses_rec  BaseCl_def)
   548 qed
   549 
   550 lemma superclassesExt [simp]: "superclasses tprg Ext={Base,Object}"
   551 proof -
   552   have ws: "ws_prog tprg" by (rule ws_tprg)
   553   then show ?thesis
   554     by (auto simp add: superclasses_rec  ExtCl_def BaseCl_def)
   555 qed
   556 
   557 lemma superclassesMain [simp]: "superclasses tprg Main={Object}"
   558 proof -
   559   have ws: "ws_prog tprg" by (rule ws_tprg)
   560   then show ?thesis
   561     by (auto simp add: superclasses_rec  MainCl_def)
   562 qed
   563 
   564 lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P" 
   565 by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def)
   566 
   567 lemma HasFoo_is_acc_iface[simp]: "is_acc_iface tprg P HasFoo"
   568 by (simp add: is_acc_iface_def)
   569 
   570 lemma HasFoo_is_acc_type[simp]: "is_acc_type tprg P (Iface HasFoo)"
   571 by (simp add: is_acc_type_def)
   572 
   573 lemma Base_accessible[simp]:"tprg\<turnstile>(Class Base) accessible_in P" 
   574 by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def)
   575 
   576 lemma Base_is_acc_class[simp]: "is_acc_class tprg P Base"
   577 by (simp add: is_acc_class_def)
   578 
   579 lemma Base_is_acc_type[simp]: "is_acc_type tprg P (Class Base)"
   580 by (simp add: is_acc_type_def)
   581 
   582 lemma Ext_accessible[simp]:"tprg\<turnstile>(Class Ext) accessible_in P" 
   583 by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def)
   584 
   585 lemma Ext_is_acc_class[simp]: "is_acc_class tprg P Ext"
   586 by (simp add: is_acc_class_def)
   587 
   588 lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)"
   589 by (simp add: is_acc_type_def)
   590 
   591 lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty"
   592 apply (unfold accmethd_def)
   593 apply (simp)
   594 done
   595 
   596 lemma  snd_special_simp: "snd ((\<lambda>(s, m). (s, a, m)) x) = (a,snd x)"
   597 by (cases x) (auto)
   598 
   599 lemma  fst_special_simp: "fst ((\<lambda>(s, m). (s, a, m)) x) = fst x"
   600 by (cases x) (auto)
   601 
   602 lemma foo_sig_undeclared_in_Object:
   603   "tprg\<turnstile>mid foo_sig undeclared_in Object"
   604 by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def)
   605 
   606 lemma unique_sig_Base_foo:
   607  "tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base \<Longrightarrow> sig=foo_sig"
   608 by (auto simp add: declared_in_def cdeclaredmethd_def 
   609                    Base_foo_def BaseCl_def)
   610 
   611 lemma Base_foo_no_override:
   612  "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides old \<Longrightarrow> P"
   613 apply (drule overrides_commonD)
   614 apply (clarsimp)
   615 apply (frule subclsEval)
   616 apply    (rule ws_tprg)
   617 apply    (simp)
   618 apply    (rule classesDefined) 
   619 apply    assumption+
   620 apply (frule unique_sig_Base_foo) 
   621 apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
   622             dest: unique_sig_Base_foo)
   623 done
   624 
   625 lemma Base_foo_no_stat_override:
   626  "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides\<^sub>S old \<Longrightarrow> P"
   627 apply (drule stat_overrides_commonD)
   628 apply (clarsimp)
   629 apply (frule subclsEval)
   630 apply    (rule ws_tprg)
   631 apply    (simp)
   632 apply    (rule classesDefined) 
   633 apply    assumption+
   634 apply (frule unique_sig_Base_foo) 
   635 apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
   636             dest: unique_sig_Base_foo)
   637 done
   638 
   639 
   640 lemma Base_foo_no_hide:
   641  "tprg,sig\<turnstile>(Base,(snd Base_foo)) hides old \<Longrightarrow> P"
   642 by (auto dest: hidesD simp add: Base_foo_def member_is_static_simp)
   643 
   644 lemma Ext_foo_no_hide:
   645  "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) hides old \<Longrightarrow> P"
   646 by (auto dest: hidesD simp add: Ext_foo_def member_is_static_simp)
   647 
   648 lemma unique_sig_Ext_foo:
   649  "tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext \<Longrightarrow> sig=foo_sig"
   650 by (auto simp add: declared_in_def cdeclaredmethd_def 
   651                    Ext_foo_def ExtCl_def)
   652 
   653 lemma Ext_foo_override:
   654  "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old 
   655   \<Longrightarrow> old = (Base,(snd Base_foo))"
   656 apply (drule overrides_commonD)
   657 apply (clarsimp)
   658 apply (frule subclsEval)
   659 apply    (rule ws_tprg)
   660 apply    (simp)
   661 apply    (rule classesDefined) 
   662 apply    assumption+
   663 apply (frule unique_sig_Ext_foo) 
   664 apply (case_tac "old")
   665 apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
   666 apply (auto simp add: ExtCl_def Ext_foo_def
   667                       BaseCl_def Base_foo_def Object_mdecls_def
   668                       split_paired_all
   669                       member_is_static_simp
   670            dest: declared_not_undeclared unique_declaration)
   671 done
   672 
   673 lemma Ext_foo_stat_override:
   674  "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides\<^sub>S old 
   675   \<Longrightarrow> old = (Base,(snd Base_foo))"
   676 apply (drule stat_overrides_commonD)
   677 apply (clarsimp)
   678 apply (frule subclsEval)
   679 apply    (rule ws_tprg)
   680 apply    (simp)
   681 apply    (rule classesDefined) 
   682 apply    assumption+
   683 apply (frule unique_sig_Ext_foo) 
   684 apply (case_tac "old")
   685 apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
   686 apply (auto simp add: ExtCl_def Ext_foo_def
   687                       BaseCl_def Base_foo_def Object_mdecls_def
   688                       split_paired_all
   689                       member_is_static_simp
   690            dest: declared_not_undeclared unique_declaration)
   691 done
   692 
   693 lemma Base_foo_member_of_Base: 
   694   "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
   695 by (auto intro!: members.Immediate Base_declares_foo)
   696 
   697 lemma Base_foo_member_in_Base: 
   698   "tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
   699 by (rule member_of_to_member_in [OF Base_foo_member_of_Base])
   700 
   701 lemma Ext_foo_member_of_Ext: 
   702   "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
   703 by (auto intro!: members.Immediate Ext_declares_foo)
   704 
   705 lemma Ext_foo_member_in_Ext: 
   706   "tprg\<turnstile>(Ext,mdecl Ext_foo) member_in Ext"
   707 by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])
   708 
   709 lemma Base_foo_permits_acc:
   710  "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_from S"
   711 by ( simp add: permits_acc_def Base_foo_def)
   712 
   713 lemma Base_foo_accessible [simp]:
   714  "tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S"
   715 by (auto intro: accessible_fromR.Immediate 
   716                 Base_foo_member_of_Base Base_foo_permits_acc)
   717 
   718 lemma Base_foo_dyn_accessible [simp]:
   719  "tprg\<turnstile>(Base,mdecl Base_foo) in Base dyn_accessible_from S"
   720 apply (rule dyn_accessible_fromR.Immediate)
   721 apply   (rule Base_foo_member_in_Base)
   722 apply   (rule Base_foo_permits_acc)
   723 done
   724 
   725 lemma accmethd_Base [simp]: 
   726   "accmethd tprg S Base = methd tprg Base"
   727 apply (simp add: accmethd_def)
   728 apply (rule filter_tab_all_True)
   729 apply (simp add: snd_special_simp fst_special_simp)
   730 done
   731 
   732 lemma Ext_foo_permits_acc:
   733  "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_from S"
   734 by ( simp add: permits_acc_def Ext_foo_def)
   735 
   736 lemma Ext_foo_accessible [simp]:
   737  "tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S"
   738 by (auto intro: accessible_fromR.Immediate 
   739                 Ext_foo_member_of_Ext Ext_foo_permits_acc)
   740 
   741 lemma Ext_foo_dyn_accessible [simp]:
   742  "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from S"
   743 apply (rule dyn_accessible_fromR.Immediate) 
   744 apply   (rule Ext_foo_member_in_Ext)
   745 apply   (rule Ext_foo_permits_acc)
   746 done
   747 
   748 lemma Ext_foo_overrides_Base_foo:
   749  "tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)"
   750 proof (rule overridesR.Direct, simp_all)
   751   show "\<not> is_static Ext_foo" 
   752     by (simp add: member_is_static_simp Ext_foo_def)
   753   show "\<not> is_static Base_foo"
   754     by (simp add: member_is_static_simp Base_foo_def)
   755   show "accmodi Ext_foo \<noteq> Private"
   756     by (simp add: Ext_foo_def)
   757   show "msig (Ext, Ext_foo) = msig (Base, Base_foo)"
   758     by (simp add: Ext_foo_def Base_foo_def)
   759   show "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
   760     by (auto intro: Ext_declares_foo)
   761   show "tprg\<turnstile>mdecl Base_foo declared_in Base"
   762     by (auto intro: Base_declares_foo)
   763   show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang"
   764     by (simp add: inheritable_in_def Base_foo_def)
   765   show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo"
   766     by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp)
   767 qed
   768 
   769 lemma accmethd_Ext [simp]: 
   770   "accmethd tprg S Ext = methd tprg Ext"
   771 apply (simp add: accmethd_def)
   772 apply (rule filter_tab_all_True)
   773 apply (auto simp add: snd_special_simp fst_special_simp)
   774 done
   775 
   776 lemma cls_Ext: "class tprg Ext = Some ExtCl"
   777 by simp
   778 lemma dynmethd_Ext_foo:
   779  "dynmethd tprg Base Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
   780   = Some (Ext,snd Ext_foo)"
   781 proof -
   782   have "methd tprg Base \<lparr>name = foo, parTs = [Class Base]\<rparr> 
   783           = Some (Base,snd Base_foo)" and
   784        "methd tprg Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
   785           = Some (Ext,snd Ext_foo)" 
   786     by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def)
   787   with cls_Ext ws_tprg Ext_foo_overrides_Base_foo
   788   show ?thesis
   789     by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def)
   790 qed
   791 
   792 lemma Base_fields_accessible[simp]:
   793  "accfield tprg S Base 
   794   = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
   795 apply (auto simp add: accfield_def 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 section "well-formedness"
   885 
   886 
   887 lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
   888 apply (unfold wf_idecl_def HasFooInt_def)
   889 apply (auto intro!: wf_mheadI ws_idecl_HasFoo 
   890             simp add: foo_sig_def foo_mhead_def mhead_resTy_simp
   891                       member_is_static_simp )
   892 done
   893 
   894 
   895 declare member_is_static_simp [simp]
   896 declare wt.Skip [rule del] wt.Init [rule del]
   897 ML {* bind_thms ("wt_intros", map (rewrite_rule @{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 declare member_is_static_simp [simp add]
   979 
   980 lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
   981 apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
   982 apply (auto intro!: wf_Base_foo)
   983 apply        (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
   984 apply   (auto intro!: wtIs)
   985 (* for definite assignment *)
   986 apply   (rule exI)
   987 apply   (rule da.Expr)
   988 apply  (rule da.Ass)
   989 apply    (simp)
   990 apply   (rule da.FVar)
   991 apply   (rule da.Cast)
   992 apply   (rule da_Lit)
   993 apply   simp
   994 apply  (rule da.NewA)
   995 apply  (rule da.Lit)
   996 apply (auto simp add: Base_foo_defs entails_def Let_def)
   997 apply   (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+
   998 apply (insert Base_foo_no_hide         , simp add: Base_foo_def,blast)
   999 done
  1000 
  1001 
  1002 lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
  1003 apply (unfold wf_cdecl_def ExtCl_def)
  1004 apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
  1005 apply  (auto simp add: entails_def snd_special_simp)
  1006 apply      (insert Ext_foo_stat_override)
  1007 apply      (rule exI,rule da.Skip)      
  1008 apply     (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
  1009 apply    (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
  1010 apply   (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
  1011 apply  (insert Ext_foo_no_hide)
  1012 apply  (simp_all add: qmdecl_def)
  1013 apply  blast+
  1014 done
  1015 
  1016 lemma wf_MainC: "wf_cdecl tprg (Main,MainCl)"
  1017 apply (unfold wf_cdecl_def MainCl_def)
  1018 apply (auto intro: ws_cdecl_Main)
  1019 apply (rule exI,rule da.Skip)
  1020 done
  1021 
  1022 lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)"
  1023 apply (simp (no_asm) add: Ifaces_def)
  1024 apply (simp (no_asm_simp))
  1025 apply (rule wf_HasFoo)
  1026 done
  1027 
  1028 lemma wf_cdecl_all_standard_classes: 
  1029   "Ball (set standard_classes) (wf_cdecl tprg)"
  1030 apply (unfold standard_classes_def Let_def 
  1031        ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
  1032 apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
  1033 apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def 
  1034             intro: da.Skip)
  1035 apply (auto simp add: Object_def Classes_def standard_classes_def 
  1036                       SXcptC_def SXcpt_def)
  1037 done
  1038 
  1039 lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)"
  1040 apply (simp (no_asm) add: Classes_def)
  1041 apply (simp (no_asm_simp))
  1042 apply    (rule wf_BaseC [THEN conjI])
  1043 apply   (rule wf_ExtC [THEN conjI])
  1044 apply  (rule wf_MainC [THEN conjI])
  1045 apply (rule wf_cdecl_all_standard_classes)
  1046 done
  1047 
  1048 theorem wf_tprg: "wf_prog tprg"
  1049 apply (unfold wf_prog_def Let_def)
  1050 apply (simp (no_asm) add: unique_ifaces unique_classes)
  1051 apply (rule conjI)
  1052 apply  ((simp (no_asm) add: Classes_def standard_classes_def))
  1053 apply (rule conjI)
  1054 apply (simp add: Object_mdecls_def)
  1055 apply safe
  1056 apply  (cut_tac xn_cases)   
  1057 apply  (simp (no_asm_simp) add: Classes_def standard_classes_def)
  1058 apply  (insert wf_idecl_all)
  1059 apply  (insert wf_cdecl_all)
  1060 apply  auto
  1061 done
  1062 
  1063 section "max spec"
  1064 
  1065 lemma appl_methds_Base_foo: 
  1066 "appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> =  
  1067   {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
  1068     ,[Class Base])}"
  1069 apply (unfold appl_methds_def)
  1070 apply (simp (no_asm))
  1071 apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
  1072 apply  (auto simp add: cmheads_def Base_foo_defs)
  1073 done
  1074 
  1075 lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 
  1076   {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
  1077    , [Class Base])}"
  1078 by (simp add: max_spec_def appl_methds_Base_foo Collect_conv_if)
  1079 
  1080 section "well-typedness"
  1081 
  1082 schematic_lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
  1083 apply (unfold test_def arr_viewed_from_def)
  1084 (* ?pTs = [Class Base] *)
  1085 apply (rule wtIs (* ;; *))
  1086 apply  (rule wtIs (* Ass *))
  1087 apply  (rule wtIs (* NewC *))
  1088 apply     (rule wtIs (* LVar *))
  1089 apply      (simp)
  1090 apply     (simp)
  1091 apply    (simp)
  1092 apply   (rule wtIs (* NewC *))
  1093 apply   (simp)
  1094 apply  (simp)
  1095 apply (rule wtIs (* Try *))
  1096 prefer 4
  1097 apply    (simp)
  1098 defer
  1099 apply    (rule wtIs (* Expr *))
  1100 apply    (rule wtIs (* Call *))
  1101 apply       (rule wtIs (* Acc *))
  1102 apply       (rule wtIs (* LVar *))
  1103 apply        (simp)
  1104 apply       (simp)
  1105 apply      (rule wtIs (* Cons *))
  1106 apply       (rule wtIs (* Lit *))
  1107 apply       (simp)
  1108 apply      (rule wtIs (* Nil *))
  1109 apply     (simp)
  1110 apply     (rule max_spec_Base_foo)
  1111 apply    (simp)
  1112 apply   (simp)
  1113 apply  (simp)
  1114 apply  (simp)
  1115 apply  (simp)
  1116 apply (rule wtIs (* While *))
  1117 apply  (rule wtIs (* Acc *))
  1118 apply   (rule wtIs (* AVar *))
  1119 apply   (rule wtIs (* Acc *))
  1120 apply   (rule wtIs (* FVar *))
  1121 apply    (rule wtIs (* StatRef *))
  1122 apply    (simp)
  1123 apply   (simp)
  1124 apply   (simp )
  1125 apply   (simp)
  1126 apply   (simp)
  1127 apply  (rule wtIs (* LVar *))
  1128 apply  (simp)
  1129 apply (rule wtIs (* Skip *))
  1130 done
  1131 
  1132 section "definite assignment"
  1133 
  1134 schematic_lemma da_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>
  1135                   \<turnstile>{} \<guillemotright>\<langle>test ?pTs\<rangle>\<guillemotright> \<lparr>nrm={VName e},brk=\<lambda> l. UNIV\<rparr>"
  1136 apply (unfold test_def arr_viewed_from_def)
  1137 apply (rule da.Comp)
  1138 apply    (rule da.Expr)
  1139 apply    (rule da.AssLVar)
  1140 apply      (rule da.NewC)
  1141 apply     (rule assigned.select_convs)
  1142 apply    (simp)
  1143 apply   (rule da.Try)
  1144 apply      (rule da.Expr)
  1145 apply      (rule da.Call)
  1146 apply       (rule da.AccLVar)
  1147 apply         (simp)   
  1148 apply        (rule assigned.select_convs)
  1149 apply       (simp)
  1150 apply      (rule da.Cons)
  1151 apply       (rule da.Lit)
  1152 apply      (rule da.Nil)
  1153 apply     (rule da.Loop)
  1154 apply        (rule da.Acc)
  1155 apply         (simp)
  1156 apply        (rule da.AVar)
  1157 apply         (rule da.Acc)
  1158 apply          simp
  1159 apply         (rule da.FVar)
  1160 apply         (rule da.Cast)
  1161 apply         (rule da.Lit)
  1162 apply        (rule da.Lit)
  1163 apply       (rule da_Skip)
  1164 apply       (simp)
  1165 apply      (simp,rule assigned.select_convs)
  1166 apply     (simp)
  1167 apply    (simp,rule assigned.select_convs)
  1168 apply   (simp)
  1169 apply  simp
  1170 apply simp
  1171 apply (simp add: intersect_ts_def)
  1172 done
  1173 
  1174 
  1175 section "execution"
  1176 
  1177 lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>  
  1178   new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
  1179 apply (frule atleast_free_SucD)
  1180 apply (drule atleast_free_Suc [THEN iffD1])
  1181 apply clarsimp
  1182 apply (frule new_Addr_SomeI)
  1183 apply force
  1184 done
  1185 
  1186 declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
  1187 declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
  1188 declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
  1189         Base_foo_defs  [simp]
  1190 
  1191 ML {* bind_thms ("eval_intros", map 
  1192         (simplify (@{simpset} delsimps @{thms Skip_eq}
  1193                              addsimps @{thms lvar_def}) o 
  1194          rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}
  1195 lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
  1196 
  1197 axiomatization
  1198   a :: loc and
  1199   b :: loc and
  1200   c :: loc
  1201 
  1202 abbreviation "one == Suc 0"
  1203 abbreviation "two == Suc one"
  1204 abbreviation "three == Suc two"
  1205 abbreviation "four == Suc three"
  1206 
  1207 abbreviation
  1208   "obj_a == \<lparr>tag=Arr (PrimT Boolean) 2
  1209                 ,values= empty(Inr 0\<mapsto>Bool False)(Inr 1\<mapsto>Bool False)\<rparr>"
  1210 
  1211 abbreviation
  1212   "obj_b == \<lparr>tag=CInst Ext
  1213                 ,values=(empty(Inl (vee, Base)\<mapsto>Null   )
  1214                               (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
  1215 
  1216 abbreviation
  1217   "obj_c == \<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
  1218 
  1219 abbreviation "arr_N == empty(Inl (arr, Base)\<mapsto>Null)"
  1220 abbreviation "arr_a == empty(Inl (arr, Base)\<mapsto>Addr a)"
  1221 
  1222 abbreviation
  1223   "globs1 == empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
  1224                      (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_N\<rparr>)
  1225                      (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)"
  1226 
  1227 abbreviation
  1228   "globs2 == empty(Inr Ext   \<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
  1229                      (Inr Object\<mapsto>\<lparr>tag=undefined, values=empty\<rparr>)
  1230                      (Inl a\<mapsto>obj_a)
  1231                      (Inr Base  \<mapsto>\<lparr>tag=undefined, values=arr_a\<rparr>)"
  1232 
  1233 abbreviation "globs3 == globs2(Inl b\<mapsto>obj_b)"
  1234 abbreviation "globs8 == globs3(Inl c\<mapsto>obj_c)"
  1235 abbreviation "locs3 == empty(VName e\<mapsto>Addr b)"
  1236 abbreviation "locs8 == locs3(VName z\<mapsto>Addr c)"
  1237 
  1238 abbreviation "s0 == st empty empty"
  1239 abbreviation "s0' == Norm  s0"
  1240 abbreviation "s1 == st globs1 empty"
  1241 abbreviation "s1' == Norm s1"
  1242 abbreviation "s2 == st globs2 empty"
  1243 abbreviation "s2' == Norm s2"
  1244 abbreviation "s3 == st globs3 locs3"
  1245 abbreviation "s3' == Norm s3"
  1246 abbreviation "s7' == (Some (Xcpt (Std NullPointer)), s3)"
  1247 abbreviation "s8 == st globs8 locs8"
  1248 abbreviation "s8' == Norm s8"
  1249 abbreviation "s9' == (Some (Xcpt (Std IndOutBound)), s8)"
  1250 
  1251 
  1252 declare Pair_eq [simp del]
  1253 schematic_lemma exec_test: 
  1254 "\<lbrakk>the (new_Addr (heap  s1)) = a;  
  1255   the (new_Addr (heap ?s2)) = b;  
  1256   the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>  
  1257   atleast_free  (heap s0) four \<Longrightarrow>  
  1258   tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'"
  1259 apply (unfold test_def arr_viewed_from_def)
  1260 (* ?s9' = s9' *)
  1261 apply (simp (no_asm_use))
  1262 apply (drule (1) alloc_one,clarsimp)
  1263 apply (rule eval_Is (* ;; *))
  1264 apply  (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
  1265 apply  (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
  1266 apply  (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
  1267 apply  (rule eval_Is (* Expr *))
  1268 apply  (rule eval_Is (* Ass *))
  1269 apply   (rule eval_Is (* LVar *))
  1270 apply  (rule eval_Is (* NewC *))
  1271       (* begin init Ext *)
  1272 apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
  1273 apply   (erule_tac V = "atleast_free ?h three" in thin_rl)
  1274 apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
  1275 apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
  1276 apply   (rule eval_Is (* Init Ext *))
  1277 apply   (simp)
  1278 apply   (rule conjI)
  1279 prefer 2 apply (rule conjI HOL.refl)+
  1280 apply   (rule eval_Is (* Init Base *))
  1281 apply   (simp add: arr_viewed_from_def)
  1282 apply   (rule conjI)
  1283 apply    (rule eval_Is (* Init Object *))
  1284 apply    (simp)
  1285 apply    (rule conjI, rule HOL.refl)+
  1286 apply    (rule HOL.refl)
  1287 apply   (simp)
  1288 apply   (rule conjI, rule_tac [2] HOL.refl)
  1289 apply   (rule eval_Is (* Expr *))
  1290 apply   (rule eval_Is (* Ass *))
  1291 apply    (rule eval_Is (* FVar *))
  1292 apply         (rule init_done, simp)
  1293 apply        (rule eval_Is (* StatRef *))
  1294 apply       (simp)
  1295 apply     (simp add: check_field_access_def Let_def) 
  1296 apply   (rule eval_Is (* NewA *))
  1297 apply     (simp)
  1298 apply    (rule eval_Is (* Lit *))
  1299 apply   (simp)
  1300 apply   (rule halloc.New)
  1301 apply    (simp (no_asm_simp))
  1302 apply   (drule atleast_free_weaken,drule atleast_free_weaken)
  1303 apply   (simp (no_asm_simp))
  1304 apply  (simp add: upd_gobj_def)
  1305       (* end init Ext *)
  1306 apply  (rule halloc.New)
  1307 apply   (drule alloc_one)
  1308 prefer 2 apply fast
  1309 apply   (simp (no_asm_simp))
  1310 apply  (drule atleast_free_weaken)
  1311 apply  force
  1312 apply (simp)
  1313 apply (drule alloc_one)
  1314 apply  (simp (no_asm_simp))
  1315 apply clarsimp
  1316 apply (erule_tac V = "atleast_free ?h three" in thin_rl)
  1317 apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
  1318 apply (simp (no_asm_use))
  1319 apply (rule eval_Is (* Try *))
  1320 apply   (rule eval_Is (* Expr *))
  1321       (* begin method call *)
  1322 apply   (rule eval_Is (* Call *))
  1323 apply      (rule eval_Is (* Acc *))
  1324 apply      (rule eval_Is (* LVar *))
  1325 apply     (rule eval_Is (* Cons *))
  1326 apply      (rule eval_Is (* Lit *))
  1327 apply     (rule eval_Is (* Nil *))
  1328 apply    (simp)
  1329 apply    (simp)
  1330 apply    (subgoal_tac
  1331              "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from Main")
  1332 apply      (simp add: check_method_access_def Let_def
  1333                       invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
  1334 apply      (rule Ext_foo_dyn_accessible)
  1335 apply   (rule eval_Is (* Methd *))
  1336 apply   (simp add: body_def Let_def)
  1337 apply   (rule eval_Is (* Body *))
  1338 apply     (rule init_done, simp)
  1339 apply       (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
  1340 apply    (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
  1341 apply    (rule eval_Is (* Comp *))
  1342 apply     (rule eval_Is (* Expr *))
  1343 apply     (rule eval_Is (* Ass *))
  1344 apply      (rule eval_Is (* FVar *))
  1345 apply         (rule init_done, simp)
  1346 apply        (rule eval_Is (* Cast *))
  1347 apply         (rule eval_Is (* Acc *))
  1348 apply         (rule eval_Is (* LVar *))
  1349 apply        (simp)
  1350 apply       (simp split del: split_if)
  1351 apply      (simp add: check_field_access_def Let_def)
  1352 apply     (rule eval_Is (* XcptE *))
  1353 apply    (simp)
  1354 apply    (rule conjI)
  1355 apply     (simp)
  1356 apply    (rule eval_Is (* Comp *))
  1357 apply   (simp)
  1358       (* end method call *)
  1359 apply  simp
  1360 apply  (rule sxalloc.intros)
  1361 apply  (rule halloc.New)
  1362 apply   (erule alloc_one [THEN conjunct1])
  1363 apply   (simp (no_asm_simp))
  1364 apply  (simp (no_asm_simp))
  1365 apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
  1366 apply (drule alloc_one [THEN conjunct1])
  1367 apply  (simp (no_asm_simp))
  1368 apply (erule_tac V = "atleast_free ?h two" in thin_rl)
  1369 apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
  1370 apply simp
  1371 apply (rule eval_Is (* While *))
  1372 apply  (rule eval_Is (* Acc *))
  1373 apply  (rule eval_Is (* AVar *))
  1374 apply    (rule eval_Is (* Acc *))
  1375 apply    (rule eval_Is (* FVar *))
  1376 apply      (rule init_done, simp)
  1377 apply     (rule eval_Is (* StatRef *))
  1378 apply    (simp)
  1379 apply    (simp add: check_field_access_def Let_def)
  1380 apply   (rule eval_Is (* Lit *))
  1381 apply  (simp (no_asm_simp))
  1382 apply (auto simp add: in_bounds_def)
  1383 done
  1384 declare Pair_eq [simp]
  1385 
  1386 end