src/HOL/Bali/Example.thy
changeset 12925 99131847fb93
parent 12858 6214f03d6d27
child 13524 604d0f3622d6
     1.1 --- a/src/HOL/Bali/Example.thy	Thu Feb 21 20:11:32 2002 +0100
     1.2 +++ b/src/HOL/Bali/Example.thy	Fri Feb 22 11:26:44 2002 +0100
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  theory Example = Eval + WellForm:
     1.6  
     1.7 -
     1.8  text {*
     1.9  The following example Bali program includes:
    1.10  \begin{itemize}
    1.11 @@ -43,7 +42,7 @@
    1.12    }
    1.13  }
    1.14  
    1.15 -public class Example {
    1.16 +public class Main {
    1.17    public static void main(String args[]) throws Throwable {
    1.18      Base e = new Ext();
    1.19      try {e.foo(null); }
    1.20 @@ -54,7 +53,6 @@
    1.21  }
    1.22  \end{verbatim}
    1.23  *}
    1.24 -
    1.25  declare widen.null [intro]
    1.26  
    1.27  lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
    1.28 @@ -68,7 +66,7 @@
    1.29  section "type and expression names"
    1.30  
    1.31  (** unfortunately cannot simply instantiate tnam **)
    1.32 -datatype tnam_  = HasFoo_ | Base_ | Ext_
    1.33 +datatype tnam_  = HasFoo_ | Base_ | Ext_ | Main_
    1.34  datatype vnam_  = arr_ | vee_ | z_ | e_
    1.35  datatype label_ = lab1_
    1.36  
    1.37 @@ -94,6 +92,7 @@
    1.38    HasFoo :: qtname
    1.39    Base   :: qtname
    1.40    Ext    :: qtname
    1.41 +  Main   :: qtname
    1.42    arr :: ename
    1.43    vee :: ename
    1.44    z   :: ename
    1.45 @@ -104,6 +103,7 @@
    1.46    "HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
    1.47    "Base"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
    1.48    "Ext"    == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
    1.49 +  "Main"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Main_)\<rparr>"
    1.50    "arr"    ==        "(vnam_ arr_)"
    1.51    "vee"    ==        "(vnam_ vee_)"
    1.52    "z"      ==        "(vnam_ z_)"
    1.53 @@ -117,12 +117,18 @@
    1.54  lemma neq_Ext_Object [simp]: "Ext\<noteq>Object"
    1.55  by (simp add: Object_def)
    1.56  
    1.57 +lemma neq_Main_Object [simp]: "Main\<noteq>Object"
    1.58 +by (simp add: Object_def)
    1.59 +
    1.60  lemma neq_Base_SXcpt [simp]: "Base\<noteq>SXcpt xn"
    1.61  by (simp add: SXcpt_def)
    1.62  
    1.63  lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
    1.64  by (simp add: SXcpt_def)
    1.65  
    1.66 +lemma neq_Main_Object [simp]: "Main\<noteq>SXcpt xn"
    1.67 +by (simp add: SXcpt_def)
    1.68 +
    1.69  section "classes and interfaces"
    1.70  
    1.71  defs
    1.72 @@ -147,26 +153,28 @@
    1.73    Base_foo :: mdecl
    1.74   "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
    1.75                          mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
    1.76 -  
    1.77 +
    1.78 +constdefs
    1.79    Ext_foo  :: mdecl
    1.80   "Ext_foo  \<equiv> (foo_sig, 
    1.81                \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
    1.82  	       mbody=\<lparr>lcls=[]
    1.83 -                     ,stmt=Expr({Ext,False}Cast (Class Ext) (!!z)..vee := 
    1.84 +                     ,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := 
    1.85         	                                                     Lit (Intg 1))\<rparr>
    1.86  	      \<rparr>)"
    1.87  
    1.88  constdefs
    1.89    
    1.90 -arr_viewed_from :: "qtname \<Rightarrow> var"
    1.91 -"arr_viewed_from C \<equiv> {Base,True}StatRef (ClassT C)..arr"
    1.92 +arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var"
    1.93 +"arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr"
    1.94  
    1.95  BaseCl :: class
    1.96  "BaseCl \<equiv> \<lparr>access=Public,
    1.97             cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
    1.98  	            (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
    1.99             methods=[Base_foo],
   1.100 -           init=Expr(arr_viewed_from Base :=New (PrimT Boolean)[Lit (Intg 2)]),
   1.101 +           init=Expr(arr_viewed_from Base Base 
   1.102 +                     :=New (PrimT Boolean)[Lit (Intg 2)]),
   1.103             super=Object,
   1.104             superIfs=[HasFoo]\<rparr>"
   1.105    
   1.106 @@ -178,6 +186,15 @@
   1.107             super=Base,
   1.108             superIfs=[]\<rparr>"
   1.109  
   1.110 +MainCl :: class
   1.111 +"MainCl \<equiv> \<lparr>access=Public,
   1.112 +           cfields=[], 
   1.113 +           methods=[], 
   1.114 +           init=Skip,
   1.115 +           super=Object,
   1.116 +           superIfs=[]\<rparr>"
   1.117 +(* The "main" method is modeled seperately (see tprg) *)
   1.118 +
   1.119  constdefs
   1.120    
   1.121    HasFooInt :: iface
   1.122 @@ -187,7 +204,7 @@
   1.123   "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
   1.124  
   1.125   "Classes" ::"cdecl list"
   1.126 - "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl)]@standard_classes"
   1.127 + "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes"
   1.128  
   1.129  lemmas table_classes_defs = 
   1.130       Classes_def standard_classes_def ObjectC_def SXcptC_def
   1.131 @@ -231,6 +248,10 @@
   1.132  apply (simp (no_asm) add: Object_def SXcpt_def)
   1.133  done
   1.134  
   1.135 +lemma table_classes_Main [simp]: "table_of Classes Main = Some MainCl"
   1.136 +apply (unfold table_classes_defs )
   1.137 +apply (simp (no_asm) add: Object_def SXcpt_def)
   1.138 +done
   1.139  
   1.140  section "program"
   1.141  
   1.142 @@ -243,9 +264,10 @@
   1.143  constdefs
   1.144    test    :: "(ty)list \<Rightarrow> stmt"
   1.145   "test pTs \<equiv> e:==NewC Ext;; 
   1.146 -           \<spacespace> Try Expr({ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
   1.147 +           \<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
   1.148             \<spacespace> Catch((SXcpt NullPointer) z)
   1.149 -           (lab1\<bullet> While(Acc (Acc (arr_viewed_from Ext).[Lit (Intg 2)])) Skip)"
   1.150 +           (lab1\<bullet> While(Acc 
   1.151 +                        (Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)"
   1.152  
   1.153  
   1.154  section "well-structuredness"
   1.155 @@ -278,7 +300,7 @@
   1.156  apply (erule ssubst)
   1.157  apply (rule tnam_.induct)
   1.158  apply  safe
   1.159 -apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def)
   1.160 +apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def MainCl_def)
   1.161  apply (drule rtranclD)
   1.162  apply auto
   1.163  done
   1.164 @@ -314,8 +336,13 @@
   1.165  apply auto
   1.166  done
   1.167  
   1.168 +lemma ws_cdecl_Main: "ws_cdecl tprg Main Object"
   1.169 +apply (unfold ws_cdecl_def)
   1.170 +apply auto
   1.171 +done
   1.172 +
   1.173  lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable
   1.174 -                   ws_cdecl_Base ws_cdecl_Ext
   1.175 +                   ws_cdecl_Base ws_cdecl_Ext ws_cdecl_Main
   1.176  
   1.177  declare not_Object_subcls_any [rule del]
   1.178            not_Throwable_subcls_SXcpt [rule del] 
   1.179 @@ -329,7 +356,7 @@
   1.180  done
   1.181  
   1.182  lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,c)\<in>set Classes. ws_cdecl G C (super c))"
   1.183 -apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def)
   1.184 +apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def MainCl_def)
   1.185  apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def 
   1.186          SXcptC_def)
   1.187  done
   1.188 @@ -438,12 +465,6 @@
   1.189  apply   (auto simp add: BaseCl_def)
   1.190  done
   1.191  
   1.192 -(* ### To Table *)
   1.193 -lemma filter_tab_all_False: 
   1.194 - "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
   1.195 -by (auto simp add: filter_tab_def expand_fun_eq)
   1.196 -
   1.197 -
   1.198  lemma memberid_Base_foo_simp [simp]:
   1.199   "memberid (mdecl Base_foo) = mid foo_sig"
   1.200  by (simp add: Base_foo_def)
   1.201 @@ -504,7 +525,7 @@
   1.202  lemma classesDefined: 
   1.203   "\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc"
   1.204  apply (auto simp add: Classes_def standard_classes_def 
   1.205 -                      BaseCl_def ExtCl_def
   1.206 +                      BaseCl_def ExtCl_def MainCl_def
   1.207                        SXcptC_def ObjectC_def) 
   1.208  done
   1.209  
   1.210 @@ -522,6 +543,13 @@
   1.211      by (auto simp add: superclasses_rec  ExtCl_def BaseCl_def)
   1.212  qed
   1.213  
   1.214 +lemma superclassesMain [simp]: "superclasses tprg Main={Object}"
   1.215 +proof -
   1.216 +  have ws: "ws_prog tprg" by (rule ws_tprg)
   1.217 +  then show ?thesis
   1.218 +    by (auto simp add: superclasses_rec  MainCl_def)
   1.219 +qed
   1.220 +
   1.221  lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P" 
   1.222  by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def)
   1.223  
   1.224 @@ -564,12 +592,6 @@
   1.225    "tprg\<turnstile>mid foo_sig undeclared_in Object"
   1.226  by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def)
   1.227  
   1.228 -(* ### To DeclConcepts *)
   1.229 -lemma undeclared_not_declared:
   1.230 - "G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C" 
   1.231 -by (cases m) (auto simp add: declared_in_def undeclared_in_def)
   1.232 -
   1.233 -
   1.234  lemma unique_sig_Base_foo:
   1.235   "tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base \<Longrightarrow> sig=foo_sig"
   1.236  by (auto simp add: declared_in_def cdeclaredmethd_def 
   1.237 @@ -617,16 +639,6 @@
   1.238  by (auto simp add: declared_in_def cdeclaredmethd_def 
   1.239                     Ext_foo_def ExtCl_def)
   1.240  
   1.241 -(* ### To DeclConcepts *)
   1.242 -lemma unique_declaration: 
   1.243 - "\<lbrakk>G\<turnstile>m declared_in C;  G\<turnstile>n declared_in C; memberid m = memberid n \<rbrakk> 
   1.244 -  \<Longrightarrow> m = n"
   1.245 -apply (cases m)
   1.246 -apply (cases n,
   1.247 -        auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+
   1.248 -done
   1.249 -
   1.250 -
   1.251  lemma Ext_foo_override:
   1.252   "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old 
   1.253    \<Longrightarrow> old = (Base,(snd Base_foo))"
   1.254 @@ -667,25 +679,42 @@
   1.255             dest: declared_not_undeclared unique_declaration)
   1.256  done
   1.257  
   1.258 -(*### weiter hoch *)
   1.259  lemma Base_foo_member_of_Base: 
   1.260    "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
   1.261  by (auto intro!: members.Immediate Base_declares_foo)
   1.262  
   1.263 -(*### weiter hoch *)
   1.264 +lemma Base_foo_member_in_Base: 
   1.265 +  "tprg\<turnstile>(Base,mdecl Base_foo) member_in Base"
   1.266 +by (rule member_of_to_member_in [OF Base_foo_member_of_Base])
   1.267 +
   1.268 +lemma Base_foo_member_of_Base: 
   1.269 +  "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
   1.270 +by (auto intro!: members.Immediate Base_declares_foo)
   1.271 +
   1.272  lemma Ext_foo_member_of_Ext: 
   1.273    "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
   1.274  by (auto intro!: members.Immediate Ext_declares_foo)
   1.275  
   1.276 +lemma Ext_foo_member_in_Ext: 
   1.277 +  "tprg\<turnstile>(Ext,mdecl Ext_foo) member_in Ext"
   1.278 +by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext])
   1.279 +
   1.280  lemma Base_foo_permits_acc:
   1.281   "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
   1.282  by ( simp add: permits_acc_def Base_foo_def)
   1.283  
   1.284  lemma Base_foo_accessible [simp]:
   1.285   "tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S"
   1.286 -by (auto intro: accessible_fromR.immediate 
   1.287 +by (auto intro: accessible_fromR.Immediate 
   1.288                  Base_foo_member_of_Base Base_foo_permits_acc)
   1.289  
   1.290 +lemma Base_foo_dyn_accessible [simp]:
   1.291 + "tprg\<turnstile>(Base,mdecl Base_foo) in Base dyn_accessible_from S"
   1.292 +apply (rule dyn_accessible_fromR.Immediate)
   1.293 +apply   (rule Base_foo_member_in_Base)
   1.294 +apply   (rule Base_foo_permits_acc)
   1.295 +done
   1.296 +
   1.297  lemma accmethd_Base [simp]: 
   1.298    "accmethd tprg S Base = methd tprg Base"
   1.299  apply (simp add: accmethd_def)
   1.300 @@ -699,17 +728,15 @@
   1.301  
   1.302  lemma Ext_foo_accessible [simp]:
   1.303   "tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S"
   1.304 -by (auto intro: accessible_fromR.immediate 
   1.305 +by (auto intro: accessible_fromR.Immediate 
   1.306                  Ext_foo_member_of_Ext Ext_foo_permits_acc)
   1.307  
   1.308 -(*
   1.309 -lemma Base_foo_accessible_through_inheritance_in_Ext [simp]:
   1.310 - "tprg\<turnstile>(Base,snd Base_foo) accessible_through_inheritance_in Ext"
   1.311 -apply (rule accessible_through_inheritance.Direct)
   1.312 -apply   simp
   1.313 -apply   (simp add: accessible_for_inheritance_in_def Base_foo_def)
   1.314 +lemma Ext_foo_dyn_accessible [simp]:
   1.315 + "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from S"
   1.316 +apply (rule dyn_accessible_fromR.Immediate) 
   1.317 +apply   (rule Ext_foo_member_in_Ext)
   1.318 +apply   (rule Ext_foo_permits_acc)
   1.319  done
   1.320 -*)
   1.321  
   1.322  lemma Ext_foo_overrides_Base_foo:
   1.323   "tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)"
   1.324 @@ -732,29 +759,6 @@
   1.325      by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp)
   1.326  qed
   1.327  
   1.328 -(*
   1.329 -lemma Base_foo_of_Ext_accessible[simp]:
   1.330 - "tprg\<turnstile>(Base, mdecl Base_foo) of Ext accessible_from S"
   1.331 -apply (auto intro: accessible_fromR.immediate 
   1.332 -                Base_foo_member_of_Base Base_foo_permits_acc)
   1.333 -apply (rule accessible_fromR.immediate)
   1.334 -apply (rule_tac "old"="(Base,Base_foo)" and  sup="Base" 
   1.335 -       in accessible_fromR.overriding)
   1.336 -apply (auto intro!: Ext_foo_overrides_Base_foo)
   1.337 -apply (auto 
   1.338 -apply (insert Ext_foo_overrides_Base_foo)
   1.339 -apply (rule accessible_fromR.overriding, simp_all)
   1.340 -apply (auto intro!: Ext_foo_overrides_Base_foo)
   1.341 -apply (auto intro!: accessible_fromR.overriding
   1.342 -             intro:   Ext_foo_overrides_Base_foo)
   1.343 -by
   1.344 -                Ext_foo_member_of_Ext Ext_foo_permits_acc)
   1.345 -apply (auto intro!: accessible 
   1.346 -apply (auto simp add: method_accessible_from_def accessible_from_def) 
   1.347 -apply (simp add: Base_foo_def)
   1.348 -done 
   1.349 -*)
   1.350 -
   1.351  lemma accmethd_Ext [simp]: 
   1.352    "accmethd tprg S Ext = methd tprg Ext"
   1.353  apply (simp add: accmethd_def)
   1.354 @@ -762,7 +766,6 @@
   1.355  apply (auto simp add: snd_special_simp fst_special_simp)
   1.356  done
   1.357  
   1.358 -(* ### Weiter hoch *)
   1.359  lemma cls_Ext: "class tprg Ext = Some ExtCl"
   1.360  by simp
   1.361  lemma dynmethd_Ext_foo:
   1.362 @@ -790,7 +793,7 @@
   1.363                        declared_in_def 
   1.364                        cdeclaredfield_def
   1.365                 intro!: filter_tab_all_True_Some filter_tab_None
   1.366 -                       accessible_fromR.immediate
   1.367 +                       accessible_fromR.Immediate
   1.368                 intro: members.Immediate)
   1.369  done
   1.370  
   1.371 @@ -802,6 +805,12 @@
   1.372  by (auto intro: members.Immediate 
   1.373         simp add: declared_in_def cdeclaredfield_def BaseCl_def)
   1.374   
   1.375 +lemma arr_member_in_Base:
   1.376 +  "tprg\<turnstile>(Base, fdecl (arr, 
   1.377 +                 \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
   1.378 +          member_in Base"
   1.379 +by (rule member_of_to_member_in [OF arr_member_of_Base])
   1.380 +
   1.381  lemma arr_member_of_Ext:
   1.382    "tprg\<turnstile>(Base, fdecl (arr, 
   1.383                      \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
   1.384 @@ -812,6 +821,12 @@
   1.385  apply   (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def)
   1.386  done
   1.387  
   1.388 +lemma arr_member_in_Ext:
   1.389 +  "tprg\<turnstile>(Base, fdecl (arr, 
   1.390 +                 \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
   1.391 +          member_in Ext"
   1.392 +by (rule member_of_to_member_in [OF arr_member_of_Ext])
   1.393 +
   1.394  lemma Ext_fields_accessible[simp]:
   1.395  "accfield tprg S Ext 
   1.396    = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
   1.397 @@ -822,11 +837,27 @@
   1.398                        ExtCl_def
   1.399                        permits_acc_def
   1.400                 intro!: filter_tab_all_True_Some filter_tab_None
   1.401 -                       accessible_fromR.immediate)
   1.402 +                       accessible_fromR.Immediate)
   1.403  apply (auto intro: members.Immediate arr_member_of_Ext
   1.404              simp add: declared_in_def cdeclaredfield_def ExtCl_def)
   1.405  done
   1.406  
   1.407 +lemma arr_Base_dyn_accessible [simp]:
   1.408 +"tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
   1.409 +       in Base dyn_accessible_from S"
   1.410 +apply (rule dyn_accessible_fromR.Immediate)
   1.411 +apply   (rule arr_member_in_Base)
   1.412 +apply   (simp add: permits_acc_def)
   1.413 +done
   1.414 +
   1.415 +lemma arr_Ext_dyn_accessible[simp]:
   1.416 +"tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) 
   1.417 +       in Ext dyn_accessible_from S"
   1.418 +apply (rule dyn_accessible_fromR.Immediate)
   1.419 +apply   (rule arr_member_in_Ext)
   1.420 +apply   (simp add: permits_acc_def)
   1.421 +done
   1.422 +
   1.423  lemma array_of_PrimT_acc [simp]:
   1.424   "is_acc_type tprg java_lang (PrimT t.[])"
   1.425  apply (simp add: is_acc_type_def accessible_in_RefT_simp)
   1.426 @@ -853,6 +884,8 @@
   1.427                        member_is_static_simp )
   1.428  done
   1.429  
   1.430 +
   1.431 +declare member_is_static_simp [simp]
   1.432  declare wt.Skip [rule del] wt.Init [rule del]
   1.433  lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
   1.434  lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def
   1.435 @@ -903,6 +936,11 @@
   1.436  apply  blast+
   1.437  done
   1.438  
   1.439 +lemma wf_MainC: "wf_cdecl tprg (Main,MainCl)"
   1.440 +apply (unfold wf_cdecl_def MainCl_def)
   1.441 +apply (auto intro: ws_cdecl_Main)
   1.442 +done
   1.443 +
   1.444  lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)"
   1.445  apply (simp (no_asm) add: Ifaces_def)
   1.446  apply (simp (no_asm_simp))
   1.447 @@ -922,8 +960,9 @@
   1.448  lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)"
   1.449  apply (simp (no_asm) add: Classes_def)
   1.450  apply (simp (no_asm_simp))
   1.451 -apply   (rule wf_BaseC [THEN conjI])
   1.452 -apply  (rule wf_ExtC [THEN conjI])
   1.453 +apply    (rule wf_BaseC [THEN conjI])
   1.454 +apply   (rule wf_ExtC [THEN conjI])
   1.455 +apply  (rule wf_MainC [THEN conjI])
   1.456  apply (rule wf_cdecl_all_standard_classes)
   1.457  done
   1.458  
   1.459 @@ -966,7 +1005,7 @@
   1.460  
   1.461  section "well-typedness"
   1.462  
   1.463 -lemma wt_test: "\<lparr>prg=tprg,cls=S,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
   1.464 +lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
   1.465  apply (unfold test_def arr_viewed_from_def)
   1.466  (* ?pTs = [Class Base] *)
   1.467  apply (rule wtIs (* ;; *))
   1.468 @@ -999,6 +1038,7 @@
   1.469  apply   (simp)
   1.470  apply  (simp)
   1.471  apply  (simp)
   1.472 +apply  (simp)
   1.473  apply (rule wtIs (* While *))
   1.474  apply  (rule wtIs (* Acc *))
   1.475  apply   (rule wtIs (* AVar *))
   1.476 @@ -1009,6 +1049,7 @@
   1.477  apply   (simp)
   1.478  apply   (simp )
   1.479  apply   (simp)
   1.480 +apply   (simp)
   1.481  apply  (rule wtIs (* LVar *))
   1.482  apply  (simp)
   1.483  apply (rule wtIs (* Skip *))
   1.484 @@ -1165,9 +1206,10 @@
   1.485  apply   (rule eval_Is (* Expr *))
   1.486  apply   (rule eval_Is (* Ass *))
   1.487  apply    (rule eval_Is (* FVar *))
   1.488 -apply      (rule init_done, simp)
   1.489 -apply     (rule eval_Is (* StatRef *))
   1.490 -apply    (simp)
   1.491 +apply         (rule init_done, simp)
   1.492 +apply        (rule eval_Is (* StatRef *))
   1.493 +apply       (simp)
   1.494 +apply     (simp add: check_field_access_def Let_def) 
   1.495  apply   (rule eval_Is (* NewA *))
   1.496  apply     (simp)
   1.497  apply    (rule eval_Is (* Lit *))
   1.498 @@ -1201,7 +1243,12 @@
   1.499  apply      (rule eval_Is (* Lit *))
   1.500  apply     (rule eval_Is (* Nil *))
   1.501  apply    (simp)
   1.502 -apply   (simp)
   1.503 +apply    (simp)
   1.504 +apply    (subgoal_tac
   1.505 +             "tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from Main")
   1.506 +apply      (simp add: check_method_access_def Let_def
   1.507 +                      invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
   1.508 +apply      (rule Ext_foo_dyn_accessible)
   1.509  apply   (rule eval_Is (* Methd *))
   1.510  apply   (simp add: body_def Let_def)
   1.511  apply   (rule eval_Is (* Body *))
   1.512 @@ -1216,7 +1263,8 @@
   1.513  apply       (rule eval_Is (* Acc *))
   1.514  apply       (rule eval_Is (* LVar *))
   1.515  apply      (simp)
   1.516 -apply     (simp split del: split_if)
   1.517 +apply      (simp split del: split_if)
   1.518 +apply      (simp add: check_field_access_def Let_def)
   1.519  apply    (rule eval_Is (* XcptE *))
   1.520  apply   (simp)
   1.521        (* end method call *)
   1.522 @@ -1239,6 +1287,7 @@
   1.523  apply      (rule init_done, simp)
   1.524  apply     (rule eval_Is (* StatRef *))
   1.525  apply    (simp)
   1.526 +apply    (simp add: check_field_access_def Let_def)
   1.527  apply   (rule eval_Is (* Lit *))
   1.528  apply  (simp (no_asm_simp))
   1.529  apply (auto simp add: in_bounds_def)