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