src/HOL/Bali/Example.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/Example.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,1248 @@
     1.4 +(*  Title:      isabelle/Bali/Example.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +header {* Example Bali program *}
    1.10 +
    1.11 +theory Example = Eval + WellForm:
    1.12 +
    1.13 +
    1.14 +text {*
    1.15 +The following example Bali program includes:
    1.16 +\begin{itemize}
    1.17 +\item class and interface declarations with inheritance, hiding of fields,
    1.18 +    overriding of methods (with refined result type), array type,
    1.19 +\item method call (with dynamic binding), parameter access, return expressions,
    1.20 +\item expression statements, sequential composition, literal values, 
    1.21 +    local assignment, local access, field assignment, type cast,
    1.22 +\item exception generation and propagation, try and catch statement, throw 
    1.23 +      statement
    1.24 +\item instance creation and (default) static initialization
    1.25 +\end{itemize}
    1.26 +\begin{verbatim}
    1.27 +package java_lang
    1.28 +
    1.29 +public interface HasFoo {
    1.30 +  public Base foo(Base z);
    1.31 +}
    1.32 +
    1.33 +public class Base implements HasFoo {
    1.34 +  static boolean arr[] = new boolean[2];
    1.35 +  public HasFoo vee;
    1.36 +  public Base foo(Base z) {
    1.37 +    return z;
    1.38 +  }
    1.39 +}
    1.40 +
    1.41 +public class Ext extends Base {
    1.42 +  public int vee;
    1.43 +  public Ext foo(Base z) {
    1.44 +    ((Ext)z).vee = 1;
    1.45 +    return null;
    1.46 +  }
    1.47 +}
    1.48 +
    1.49 +public class Example {
    1.50 +  public static void main(String args[]) throws Throwable {
    1.51 +    Base e = new Ext();
    1.52 +    try {e.foo(null); }
    1.53 +    catch(NullPointerException z) { 
    1.54 +      while(Ext.arr[2]) ;
    1.55 +    }
    1.56 +  }
    1.57 +}
    1.58 +\end{verbatim}
    1.59 +*}
    1.60 +
    1.61 +declare widen.null [intro]
    1.62 +
    1.63 +lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
    1.64 +apply (unfold wf_fdecl_def)
    1.65 +apply (simp (no_asm))
    1.66 +done
    1.67 +
    1.68 +declare wf_fdecl_def2 [iff]
    1.69 +
    1.70 +
    1.71 +section "type and expression names"
    1.72 +
    1.73 +(** unfortunately cannot simply instantiate tnam **)
    1.74 +datatype tnam_  = HasFoo_ | Base_ | Ext_
    1.75 +datatype vnam_  = arr_ | vee_ | z_ | e_
    1.76 +datatype label_ = lab1_
    1.77 +
    1.78 +consts
    1.79 +
    1.80 +  tnam_ :: "tnam_  \<Rightarrow> tnam"
    1.81 +  vnam_ :: "vnam_  \<Rightarrow> vname"
    1.82 +  label_:: "label_ \<Rightarrow> label"
    1.83 +axioms  (** tnam_, vnam_ and label are intended to be isomorphic 
    1.84 +            to tnam, vname and label **)
    1.85 +
    1.86 +  inj_tnam_  [simp]: "(tnam_  x = tnam_  y) = (x = y)"
    1.87 +  inj_vnam_  [simp]: "(vnam_  x = vnam_  y) = (x = y)"
    1.88 +  inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
    1.89 +  
    1.90 +  
    1.91 +  surj_tnam_:  "\<exists>m. n = tnam_  m"
    1.92 +  surj_vnam_:  "\<exists>m. n = vnam_  m"
    1.93 +  surj_label_:" \<exists>m. n = label_ m"
    1.94 +
    1.95 +syntax
    1.96 +
    1.97 +  HasFoo :: qtname
    1.98 +  Base   :: qtname
    1.99 +  Ext    :: qtname
   1.100 +  arr :: ename
   1.101 +  vee :: ename
   1.102 +  z   :: ename
   1.103 +  e   :: ename
   1.104 +  lab1:: label
   1.105 +translations
   1.106 +
   1.107 +  "HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
   1.108 +  "Base"   == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
   1.109 +  "Ext"    == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
   1.110 +  "arr"    ==        "(vnam_ arr_)"
   1.111 +  "vee"    ==        "(vnam_ vee_)"
   1.112 +  "z"      ==        "(vnam_ z_)"
   1.113 +  "e"      ==        "(vnam_ e_)"
   1.114 +  "lab1"   ==        "label_ lab1_"
   1.115 +
   1.116 +
   1.117 +lemma neq_Base_Object [simp]: "Base\<noteq>Object"
   1.118 +by (simp add: Object_def)
   1.119 +
   1.120 +lemma neq_Ext_Object [simp]: "Ext\<noteq>Object"
   1.121 +by (simp add: Object_def)
   1.122 +
   1.123 +lemma neq_Base_SXcpt [simp]: "Base\<noteq>SXcpt xn"
   1.124 +by (simp add: SXcpt_def)
   1.125 +
   1.126 +lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn"
   1.127 +by (simp add: SXcpt_def)
   1.128 +
   1.129 +section "classes and interfaces"
   1.130 +
   1.131 +defs
   1.132 +
   1.133 +  Object_mdecls_def: "Object_mdecls \<equiv> []"
   1.134 +  SXcpt_mdecls_def:  "SXcpt_mdecls  \<equiv> []"
   1.135 +
   1.136 +consts
   1.137 +  
   1.138 +  foo    :: mname
   1.139 +
   1.140 +constdefs
   1.141 +  
   1.142 +  foo_sig   :: sig
   1.143 + "foo_sig   \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>"
   1.144 +  
   1.145 +  foo_mhead :: mhead
   1.146 + "foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>"
   1.147 +
   1.148 +constdefs
   1.149 +  
   1.150 +  Base_foo :: mdecl
   1.151 + "Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base,
   1.152 +                        mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)"
   1.153 +  
   1.154 +  Ext_foo  :: mdecl
   1.155 + "Ext_foo  \<equiv> (foo_sig, 
   1.156 +              \<lparr>access=Public,static=False,pars=[z],resT=Class Ext,
   1.157 +	       mbody=\<lparr>lcls=[]
   1.158 +                     ,stmt=Expr({Ext,False}Cast (Class Ext) (!!z)..vee := 
   1.159 +       	                                                     Lit (Intg 1))\<rparr>
   1.160 +	      \<rparr>)"
   1.161 +
   1.162 +constdefs
   1.163 +  
   1.164 +arr_viewed_from :: "qtname \<Rightarrow> var"
   1.165 +"arr_viewed_from C \<equiv> {Base,True}StatRef (ClassT C)..arr"
   1.166 +
   1.167 +BaseCl :: class
   1.168 +"BaseCl \<equiv> \<lparr>access=Public,
   1.169 +           cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
   1.170 +	            (vee, \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)],
   1.171 +           methods=[Base_foo],
   1.172 +           init=Expr(arr_viewed_from Base :=New (PrimT Boolean)[Lit (Intg 2)]),
   1.173 +           super=Object,
   1.174 +           superIfs=[HasFoo]\<rparr>"
   1.175 +  
   1.176 +ExtCl  :: class
   1.177 +"ExtCl  \<equiv> \<lparr>access=Public,
   1.178 +           cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], 
   1.179 +           methods=[Ext_foo],
   1.180 +           init=Skip,
   1.181 +           super=Base,
   1.182 +           superIfs=[]\<rparr>"
   1.183 +
   1.184 +constdefs
   1.185 +  
   1.186 +  HasFooInt :: iface
   1.187 + "HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>"
   1.188 +
   1.189 +  Ifaces ::"idecl list"
   1.190 + "Ifaces \<equiv> [(HasFoo,HasFooInt)]"
   1.191 +
   1.192 + "Classes" ::"cdecl list"
   1.193 + "Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl)]@standard_classes"
   1.194 +
   1.195 +lemmas table_classes_defs = 
   1.196 +     Classes_def standard_classes_def ObjectC_def SXcptC_def
   1.197 +
   1.198 +lemma table_ifaces [simp]: "table_of Ifaces = empty(HasFoo\<mapsto>HasFooInt)"
   1.199 +apply (unfold Ifaces_def)
   1.200 +apply (simp (no_asm))
   1.201 +done
   1.202 +
   1.203 +lemma table_classes_Object [simp]: 
   1.204 + "table_of Classes Object = Some \<lparr>access=Public,cfields=[]
   1.205 +                                 ,methods=Object_mdecls
   1.206 +                                 ,init=Skip,super=arbitrary,superIfs=[]\<rparr>"
   1.207 +apply (unfold table_classes_defs)
   1.208 +apply (simp (no_asm) add:Object_def)
   1.209 +done
   1.210 +
   1.211 +lemma table_classes_SXcpt [simp]: 
   1.212 +  "table_of Classes (SXcpt xn) 
   1.213 +    = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
   1.214 +            init=Skip,
   1.215 +            super=if xn = Throwable then Object else SXcpt Throwable,
   1.216 +            superIfs=[]\<rparr>"
   1.217 +apply (unfold table_classes_defs)
   1.218 +apply (induct_tac xn)
   1.219 +apply (simp add: Object_def SXcpt_def)+
   1.220 +done
   1.221 +
   1.222 +lemma table_classes_HasFoo [simp]: "table_of Classes HasFoo = None"
   1.223 +apply (unfold table_classes_defs)
   1.224 +apply (simp (no_asm) add: Object_def SXcpt_def)
   1.225 +done
   1.226 +
   1.227 +lemma table_classes_Base [simp]: "table_of Classes Base = Some BaseCl"
   1.228 +apply (unfold table_classes_defs )
   1.229 +apply (simp (no_asm) add: Object_def SXcpt_def)
   1.230 +done
   1.231 +
   1.232 +lemma table_classes_Ext [simp]: "table_of Classes Ext = Some ExtCl"
   1.233 +apply (unfold table_classes_defs )
   1.234 +apply (simp (no_asm) add: Object_def SXcpt_def)
   1.235 +done
   1.236 +
   1.237 +
   1.238 +section "program"
   1.239 +
   1.240 +syntax
   1.241 +  tprg :: prog
   1.242 +
   1.243 +translations
   1.244 +  "tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
   1.245 +
   1.246 +constdefs
   1.247 +  test    :: "(ty)list \<Rightarrow> stmt"
   1.248 + "test pTs \<equiv> e:==NewC Ext;; 
   1.249 +           \<spacespace> Try Expr({ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))
   1.250 +           \<spacespace> Catch((SXcpt NullPointer) z)
   1.251 +           (lab1\<bullet> While(Acc (Acc (arr_viewed_from Ext).[Lit (Intg 2)])) Skip)"
   1.252 +
   1.253 +
   1.254 +section "well-structuredness"
   1.255 +
   1.256 +lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
   1.257 +apply (auto dest!: tranclD subcls1D)
   1.258 +done
   1.259 +
   1.260 +lemma not_Throwable_subcls_SXcpt [elim!]: 
   1.261 +  "(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
   1.262 +apply (auto dest!: tranclD subcls1D) 
   1.263 +apply (simp add: Object_def SXcpt_def)
   1.264 +done
   1.265 +
   1.266 +lemma not_SXcpt_n_subcls_SXcpt_n [elim!]: 
   1.267 +  "(SXcpt xn, SXcpt xn)  \<in> (subcls1 tprg)^+ \<Longrightarrow> R"
   1.268 +apply (auto dest!: tranclD subcls1D)
   1.269 +apply (drule rtranclD)
   1.270 +apply auto
   1.271 +done
   1.272 +
   1.273 +lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+  \<Longrightarrow> R"
   1.274 +apply (auto dest!: tranclD subcls1D simp add: BaseCl_def)
   1.275 +done
   1.276 +
   1.277 +lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]: 
   1.278 +  "(\<lparr>pid=java_lang,tid=TName tn\<rparr>, \<lparr>pid=java_lang,tid=TName tn\<rparr>) 
   1.279 +   \<in> (subcls1 tprg)^+ \<longrightarrow> R"
   1.280 +apply (rule_tac n1 = "tn" in surj_tnam_ [THEN exE])
   1.281 +apply (erule ssubst)
   1.282 +apply (rule tnam_.induct)
   1.283 +apply  safe
   1.284 +apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def)
   1.285 +apply (drule rtranclD)
   1.286 +apply auto
   1.287 +done
   1.288 +
   1.289 +
   1.290 +lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []"
   1.291 +apply (unfold ws_idecl_def)
   1.292 +apply (simp (no_asm))
   1.293 +done
   1.294 +
   1.295 +lemma ws_cdecl_Object: "ws_cdecl tprg Object any"
   1.296 +apply (unfold ws_cdecl_def)
   1.297 +apply auto
   1.298 +done
   1.299 +
   1.300 +lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object"
   1.301 +apply (unfold ws_cdecl_def)
   1.302 +apply auto
   1.303 +done
   1.304 +
   1.305 +lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)"
   1.306 +apply (unfold ws_cdecl_def)
   1.307 +apply auto
   1.308 +done
   1.309 +
   1.310 +lemma ws_cdecl_Base: "ws_cdecl tprg Base Object"
   1.311 +apply (unfold ws_cdecl_def)
   1.312 +apply auto
   1.313 +done
   1.314 +
   1.315 +lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base"
   1.316 +apply (unfold ws_cdecl_def)
   1.317 +apply auto
   1.318 +done
   1.319 +
   1.320 +lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable
   1.321 +                   ws_cdecl_Base ws_cdecl_Ext
   1.322 +
   1.323 +declare not_Object_subcls_any [rule del]
   1.324 +          not_Throwable_subcls_SXcpt [rule del] 
   1.325 +          not_SXcpt_n_subcls_SXcpt_n [rule del] 
   1.326 +          not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del]
   1.327 +
   1.328 +lemma ws_idecl_all: 
   1.329 + "G=tprg \<Longrightarrow> (\<forall>(I,i)\<in>set Ifaces. ws_idecl G I (isuperIfs i))"
   1.330 +apply (simp (no_asm) add: Ifaces_def HasFooInt_def)
   1.331 +apply (auto intro!: ws_idecl_HasFoo)
   1.332 +done
   1.333 +
   1.334 +lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,c)\<in>set Classes. ws_cdecl G C (super c))"
   1.335 +apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def)
   1.336 +apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def 
   1.337 +        SXcptC_def)
   1.338 +done
   1.339 +
   1.340 +lemma ws_tprg: "ws_prog tprg"
   1.341 +apply (unfold ws_prog_def)
   1.342 +apply (auto intro!: ws_idecl_all ws_cdecl_all)
   1.343 +done
   1.344 +
   1.345 +
   1.346 +section "misc program properties (independent of well-structuredness)"
   1.347 +
   1.348 +lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)"
   1.349 +apply (unfold Ifaces_def)
   1.350 +apply (simp (no_asm))
   1.351 +done
   1.352 +
   1.353 +lemma empty_subint1 [simp]: "subint1 tprg = {}"
   1.354 +apply (unfold subint1_def Ifaces_def HasFooInt_def)
   1.355 +apply auto
   1.356 +done
   1.357 +
   1.358 +lemma unique_ifaces: "unique Ifaces"
   1.359 +apply (unfold Ifaces_def)
   1.360 +apply (simp (no_asm))
   1.361 +done
   1.362 +
   1.363 +lemma unique_classes: "unique Classes"
   1.364 +apply (unfold table_classes_defs )
   1.365 +apply (simp )
   1.366 +done
   1.367 +
   1.368 +lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
   1.369 +apply (rule SXcpt_subcls_Throwable_lemma)
   1.370 +apply auto
   1.371 +done
   1.372 +
   1.373 +lemma Ext_subclseq_Base [simp]: "tprg\<turnstile>Ext \<preceq>\<^sub>C Base"
   1.374 +apply (rule subcls_direct1)
   1.375 +apply  (simp (no_asm) add: ExtCl_def)
   1.376 +apply  (simp add: Object_def)
   1.377 +apply (simp (no_asm))
   1.378 +done
   1.379 +
   1.380 +lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<prec>\<^sub>C Base"
   1.381 +apply (rule subcls_direct2)
   1.382 +apply  (simp (no_asm) add: ExtCl_def)
   1.383 +apply  (simp add: Object_def)
   1.384 +apply (simp (no_asm))
   1.385 +done
   1.386 +
   1.387 +
   1.388 +
   1.389 +section "fields and method lookup"
   1.390 +
   1.391 +lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []"
   1.392 +by (rule ws_tprg [THEN fields_emptyI], force+)
   1.393 +
   1.394 +lemma fields_tprg_Throwable [simp]: 
   1.395 +  "DeclConcepts.fields tprg (SXcpt Throwable) = []"
   1.396 +by (rule ws_tprg [THEN fields_emptyI], force+)
   1.397 +
   1.398 +lemma fields_tprg_SXcpt [simp]: "DeclConcepts.fields tprg (SXcpt xn) = []"
   1.399 +apply (case_tac "xn = Throwable")
   1.400 +apply  (simp (no_asm_simp))
   1.401 +by (rule ws_tprg [THEN fields_emptyI], force+)
   1.402 +
   1.403 +lemmas fields_rec_ = fields_rec [OF _ ws_tprg]
   1.404 +
   1.405 +lemma fields_Base [simp]: 
   1.406 +"DeclConcepts.fields tprg Base 
   1.407 +  = [((arr,Base), \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>),
   1.408 +     ((vee,Base), \<lparr>access=Public,static=False,type=Iface HasFoo    \<rparr>)]"
   1.409 +apply (subst fields_rec_)
   1.410 +apply   (auto simp add: BaseCl_def)
   1.411 +done
   1.412 +
   1.413 +lemma fields_Ext [simp]: 
   1.414 + "DeclConcepts.fields tprg Ext  
   1.415 +  = [((vee,Ext), \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)] 
   1.416 +    @ DeclConcepts.fields tprg Base"
   1.417 +apply (rule trans)
   1.418 +apply (rule fields_rec_)
   1.419 +apply   (auto simp add: ExtCl_def Object_def)
   1.420 +done
   1.421 +
   1.422 +lemmas imethds_rec_ = imethds_rec [OF _ ws_tprg]
   1.423 +lemmas methd_rec_  = methd_rec  [OF _ ws_tprg]
   1.424 +
   1.425 +lemma imethds_HasFoo [simp]: 
   1.426 +  "imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))"
   1.427 +apply (rule trans)
   1.428 +apply (rule imethds_rec_)
   1.429 +apply  (auto simp add: HasFooInt_def)
   1.430 +done
   1.431 +
   1.432 +lemma methd_tprg_Object [simp]: "methd tprg Object = empty"
   1.433 +apply (subst methd_rec_)
   1.434 +apply (auto simp add: Object_mdecls_def)
   1.435 +done
   1.436 +
   1.437 +lemma methd_Base [simp]: 
   1.438 +  "methd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]"
   1.439 +apply (rule trans)
   1.440 +apply (rule methd_rec_)
   1.441 +apply   (auto simp add: BaseCl_def)
   1.442 +done
   1.443 +
   1.444 +(* ### To Table *)
   1.445 +lemma filter_tab_all_False: 
   1.446 + "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
   1.447 +by (auto simp add: filter_tab_def expand_fun_eq)
   1.448 +
   1.449 +
   1.450 +lemma memberid_Base_foo_simp [simp]:
   1.451 + "memberid (mdecl Base_foo) = mid foo_sig"
   1.452 +by (simp add: Base_foo_def)
   1.453 +
   1.454 +lemma memberid_Ext_foo_simp [simp]:
   1.455 + "memberid (mdecl Ext_foo) = mid foo_sig"
   1.456 +by (simp add: Ext_foo_def)
   1.457 +
   1.458 +lemma Base_declares_foo:
   1.459 +  "tprg\<turnstile>mdecl Base_foo declared_in Base"
   1.460 +by (auto simp add: declared_in_def cdeclaredmethd_def BaseCl_def Base_foo_def)
   1.461 +
   1.462 +lemma foo_sig_not_undeclared_in_Base:
   1.463 +  "\<not> tprg\<turnstile>mid foo_sig undeclared_in Base"
   1.464 +proof -
   1.465 +  from Base_declares_foo
   1.466 +  show ?thesis
   1.467 +    by (auto dest!: declared_not_undeclared )
   1.468 +qed
   1.469 +
   1.470 +lemma Ext_declares_foo:
   1.471 +  "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
   1.472 +by (auto simp add: declared_in_def cdeclaredmethd_def ExtCl_def Ext_foo_def)
   1.473 +
   1.474 +lemma foo_sig_not_undeclared_in_Ext:
   1.475 +  "\<not> tprg\<turnstile>mid foo_sig undeclared_in Ext"
   1.476 +proof -
   1.477 +  from Ext_declares_foo
   1.478 +  show ?thesis
   1.479 +    by (auto dest!: declared_not_undeclared )
   1.480 +qed
   1.481 +
   1.482 +lemma Base_foo_not_inherited_in_Ext:
   1.483 + "\<not> tprg \<turnstile> Ext inherits (Base,mdecl Base_foo)"
   1.484 +by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext)
   1.485 +
   1.486 +lemma Ext_method_inheritance:
   1.487 + "filter_tab (\<lambda>sig m. tprg \<turnstile> Ext inherits method sig m)
   1.488 +     (empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto>
   1.489 +      snd ((\<lambda>(s, m). (s, Base, m)) Base_foo)))
   1.490 +  = empty"
   1.491 +proof -
   1.492 +  from Base_foo_not_inherited_in_Ext
   1.493 +  show ?thesis
   1.494 +    by (auto intro: filter_tab_all_False simp add: Base_foo_def)
   1.495 +qed
   1.496 +
   1.497 +
   1.498 +lemma methd_Ext [simp]: "methd tprg Ext =   
   1.499 +  table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]"
   1.500 +apply (rule trans)
   1.501 +apply (rule methd_rec_)
   1.502 +apply   (auto simp add: ExtCl_def Object_def Ext_method_inheritance)
   1.503 +done
   1.504 +
   1.505 +section "accessibility"
   1.506 +
   1.507 +lemma classesDefined: 
   1.508 + "\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc"
   1.509 +apply (auto simp add: Classes_def standard_classes_def 
   1.510 +                      BaseCl_def ExtCl_def
   1.511 +                      SXcptC_def ObjectC_def) 
   1.512 +done
   1.513 +
   1.514 +lemma superclassesBase [simp]: "superclasses tprg Base={Object}"
   1.515 +proof -
   1.516 +  have ws: "ws_prog tprg" by (rule ws_tprg)
   1.517 +  then show ?thesis
   1.518 +    by (auto simp add: superclasses_rec  BaseCl_def)
   1.519 +qed
   1.520 +
   1.521 +lemma superclassesExt [simp]: "superclasses tprg Ext={Base,Object}"
   1.522 +proof -
   1.523 +  have ws: "ws_prog tprg" by (rule ws_tprg)
   1.524 +  then show ?thesis
   1.525 +    by (auto simp add: superclasses_rec  ExtCl_def BaseCl_def)
   1.526 +qed
   1.527 +
   1.528 +lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P" 
   1.529 +by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def)
   1.530 +
   1.531 +lemma HasFoo_is_acc_iface[simp]: "is_acc_iface tprg P HasFoo"
   1.532 +by (simp add: is_acc_iface_def)
   1.533 +
   1.534 +lemma HasFoo_is_acc_type[simp]: "is_acc_type tprg P (Iface HasFoo)"
   1.535 +by (simp add: is_acc_type_def)
   1.536 +
   1.537 +lemma Base_accessible[simp]:"tprg\<turnstile>(Class Base) accessible_in P" 
   1.538 +by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def)
   1.539 +
   1.540 +lemma Base_is_acc_class[simp]: "is_acc_class tprg P Base"
   1.541 +by (simp add: is_acc_class_def)
   1.542 +
   1.543 +lemma Base_is_acc_type[simp]: "is_acc_type tprg P (Class Base)"
   1.544 +by (simp add: is_acc_type_def)
   1.545 +
   1.546 +lemma Ext_accessible[simp]:"tprg\<turnstile>(Class Ext) accessible_in P" 
   1.547 +by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def)
   1.548 +
   1.549 +lemma Ext_is_acc_class[simp]: "is_acc_class tprg P Ext"
   1.550 +by (simp add: is_acc_class_def)
   1.551 +
   1.552 +lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)"
   1.553 +by (simp add: is_acc_type_def)
   1.554 +
   1.555 +lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty"
   1.556 +apply (unfold accmethd_def)
   1.557 +apply (simp)
   1.558 +done
   1.559 +
   1.560 +lemma  snd_special_simp: "snd ((\<lambda>(s, m). (s, a, m)) x) = (a,snd x)"
   1.561 +by (cases x) (auto)
   1.562 +
   1.563 +lemma  fst_special_simp: "fst ((\<lambda>(s, m). (s, a, m)) x) = fst x"
   1.564 +by (cases x) (auto)
   1.565 +
   1.566 +lemma foo_sig_undeclared_in_Object:
   1.567 +  "tprg\<turnstile>mid foo_sig undeclared_in Object"
   1.568 +by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def)
   1.569 +
   1.570 +(* ### To DeclConcepts *)
   1.571 +lemma undeclared_not_declared:
   1.572 + "G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C" 
   1.573 +by (cases m) (auto simp add: declared_in_def undeclared_in_def)
   1.574 +
   1.575 +
   1.576 +lemma unique_sig_Base_foo:
   1.577 + "tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base \<Longrightarrow> sig=foo_sig"
   1.578 +by (auto simp add: declared_in_def cdeclaredmethd_def 
   1.579 +                   Base_foo_def BaseCl_def)
   1.580 +
   1.581 +lemma Base_foo_no_override:
   1.582 + "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides old \<Longrightarrow> P"
   1.583 +apply (drule overrides_commonD)
   1.584 +apply (clarsimp)
   1.585 +apply (frule subclsEval)
   1.586 +apply    (rule ws_tprg)
   1.587 +apply    (simp)
   1.588 +apply    (rule classesDefined) 
   1.589 +apply    assumption+
   1.590 +apply (frule unique_sig_Base_foo) 
   1.591 +apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
   1.592 +            dest: unique_sig_Base_foo)
   1.593 +done
   1.594 +
   1.595 +lemma Base_foo_no_stat_override:
   1.596 + "tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides\<^sub>S old \<Longrightarrow> P"
   1.597 +apply (drule stat_overrides_commonD)
   1.598 +apply (clarsimp)
   1.599 +apply (frule subclsEval)
   1.600 +apply    (rule ws_tprg)
   1.601 +apply    (simp)
   1.602 +apply    (rule classesDefined) 
   1.603 +apply    assumption+
   1.604 +apply (frule unique_sig_Base_foo) 
   1.605 +apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object
   1.606 +            dest: unique_sig_Base_foo)
   1.607 +done
   1.608 +
   1.609 +
   1.610 +lemma Base_foo_no_hide:
   1.611 + "tprg,sig\<turnstile>(Base,(snd Base_foo)) hides old \<Longrightarrow> P"
   1.612 +by (auto dest: hidesD simp add: Base_foo_def member_is_static_simp)
   1.613 +
   1.614 +lemma Ext_foo_no_hide:
   1.615 + "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) hides old \<Longrightarrow> P"
   1.616 +by (auto dest: hidesD simp add: Ext_foo_def member_is_static_simp)
   1.617 +
   1.618 +lemma unique_sig_Ext_foo:
   1.619 + "tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext \<Longrightarrow> sig=foo_sig"
   1.620 +by (auto simp add: declared_in_def cdeclaredmethd_def 
   1.621 +                   Ext_foo_def ExtCl_def)
   1.622 +
   1.623 +(* ### To DeclConcepts *)
   1.624 +lemma unique_declaration: 
   1.625 + "\<lbrakk>G\<turnstile>m declared_in C;  G\<turnstile>n declared_in C; memberid m = memberid n \<rbrakk> 
   1.626 +  \<Longrightarrow> m = n"
   1.627 +apply (cases m)
   1.628 +apply (cases n,
   1.629 +        auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+
   1.630 +done
   1.631 +
   1.632 +
   1.633 +lemma Ext_foo_override:
   1.634 + "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old 
   1.635 +  \<Longrightarrow> old = (Base,(snd Base_foo))"
   1.636 +apply (drule overrides_commonD)
   1.637 +apply (clarsimp)
   1.638 +apply (frule subclsEval)
   1.639 +apply    (rule ws_tprg)
   1.640 +apply    (simp)
   1.641 +apply    (rule classesDefined) 
   1.642 +apply    assumption+
   1.643 +apply (frule unique_sig_Ext_foo) 
   1.644 +apply (case_tac "old")
   1.645 +apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
   1.646 +apply (auto simp add: ExtCl_def Ext_foo_def
   1.647 +                      BaseCl_def Base_foo_def Object_mdecls_def
   1.648 +                      split_paired_all
   1.649 +                      member_is_static_simp
   1.650 +           dest: declared_not_undeclared unique_declaration)
   1.651 +done
   1.652 +
   1.653 +lemma Ext_foo_stat_override:
   1.654 + "tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides\<^sub>S old 
   1.655 +  \<Longrightarrow> old = (Base,(snd Base_foo))"
   1.656 +apply (drule stat_overrides_commonD)
   1.657 +apply (clarsimp)
   1.658 +apply (frule subclsEval)
   1.659 +apply    (rule ws_tprg)
   1.660 +apply    (simp)
   1.661 +apply    (rule classesDefined) 
   1.662 +apply    assumption+
   1.663 +apply (frule unique_sig_Ext_foo) 
   1.664 +apply (case_tac "old")
   1.665 +apply (insert Base_declares_foo foo_sig_undeclared_in_Object) 
   1.666 +apply (auto simp add: ExtCl_def Ext_foo_def
   1.667 +                      BaseCl_def Base_foo_def Object_mdecls_def
   1.668 +                      split_paired_all
   1.669 +                      member_is_static_simp
   1.670 +           dest: declared_not_undeclared unique_declaration)
   1.671 +done
   1.672 +
   1.673 +(*### weiter hoch *)
   1.674 +lemma Base_foo_member_of_Base: 
   1.675 +  "tprg\<turnstile>(Base,mdecl Base_foo) member_of Base"
   1.676 +by (auto intro!: members.Immediate Base_declares_foo)
   1.677 +
   1.678 +(*### weiter hoch *)
   1.679 +lemma Ext_foo_member_of_Ext: 
   1.680 +  "tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext"
   1.681 +by (auto intro!: members.Immediate Ext_declares_foo)
   1.682 +
   1.683 +lemma Base_foo_permits_acc:
   1.684 + "tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S"
   1.685 +by ( simp add: permits_acc_def Base_foo_def)
   1.686 +
   1.687 +lemma Base_foo_accessible [simp]:
   1.688 + "tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S"
   1.689 +by (auto intro: accessible_fromR.immediate 
   1.690 +                Base_foo_member_of_Base Base_foo_permits_acc)
   1.691 +
   1.692 +lemma accmethd_Base [simp]: 
   1.693 +  "accmethd tprg S Base = methd tprg Base"
   1.694 +apply (simp add: accmethd_def)
   1.695 +apply (rule filter_tab_all_True)
   1.696 +apply (simp add: snd_special_simp fst_special_simp)
   1.697 +done
   1.698 +
   1.699 +lemma Ext_foo_permits_acc:
   1.700 + "tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S"
   1.701 +by ( simp add: permits_acc_def Ext_foo_def)
   1.702 +
   1.703 +lemma Ext_foo_accessible [simp]:
   1.704 + "tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S"
   1.705 +by (auto intro: accessible_fromR.immediate 
   1.706 +                Ext_foo_member_of_Ext Ext_foo_permits_acc)
   1.707 +
   1.708 +(*
   1.709 +lemma Base_foo_accessible_through_inheritance_in_Ext [simp]:
   1.710 + "tprg\<turnstile>(Base,snd Base_foo) accessible_through_inheritance_in Ext"
   1.711 +apply (rule accessible_through_inheritance.Direct)
   1.712 +apply   simp
   1.713 +apply   (simp add: accessible_for_inheritance_in_def Base_foo_def)
   1.714 +done
   1.715 +*)
   1.716 +
   1.717 +lemma Ext_foo_overrides_Base_foo:
   1.718 + "tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)"
   1.719 +proof (rule overridesR.Direct, simp_all)
   1.720 +  show "\<not> is_static Ext_foo" 
   1.721 +    by (simp add: member_is_static_simp Ext_foo_def)
   1.722 +  show "\<not> is_static Base_foo"
   1.723 +    by (simp add: member_is_static_simp Base_foo_def)
   1.724 +  show "accmodi Ext_foo \<noteq> Private"
   1.725 +    by (simp add: Ext_foo_def)
   1.726 +  show "msig (Ext, Ext_foo) = msig (Base, Base_foo)"
   1.727 +    by (simp add: Ext_foo_def Base_foo_def)
   1.728 +  show "tprg\<turnstile>mdecl Ext_foo declared_in Ext"
   1.729 +    by (auto intro: Ext_declares_foo)
   1.730 +  show "tprg\<turnstile>mdecl Base_foo declared_in Base"
   1.731 +    by (auto intro: Base_declares_foo)
   1.732 +  show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang"
   1.733 +    by (simp add: inheritable_in_def Base_foo_def)
   1.734 +  show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo"
   1.735 +    by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp)
   1.736 +qed
   1.737 +
   1.738 +(*
   1.739 +lemma Base_foo_of_Ext_accessible[simp]:
   1.740 + "tprg\<turnstile>(Base, mdecl Base_foo) of Ext accessible_from S"
   1.741 +apply (auto intro: accessible_fromR.immediate 
   1.742 +                Base_foo_member_of_Base Base_foo_permits_acc)
   1.743 +apply (rule accessible_fromR.immediate)
   1.744 +apply (rule_tac "old"="(Base,Base_foo)" and  sup="Base" 
   1.745 +       in accessible_fromR.overriding)
   1.746 +apply (auto intro!: Ext_foo_overrides_Base_foo)
   1.747 +apply (auto 
   1.748 +apply (insert Ext_foo_overrides_Base_foo)
   1.749 +apply (rule accessible_fromR.overriding, simp_all)
   1.750 +apply (auto intro!: Ext_foo_overrides_Base_foo)
   1.751 +apply (auto intro!: accessible_fromR.overriding
   1.752 +             intro:   Ext_foo_overrides_Base_foo)
   1.753 +by
   1.754 +                Ext_foo_member_of_Ext Ext_foo_permits_acc)
   1.755 +apply (auto intro!: accessible 
   1.756 +apply (auto simp add: method_accessible_from_def accessible_from_def) 
   1.757 +apply (simp add: Base_foo_def)
   1.758 +done 
   1.759 +*)
   1.760 +
   1.761 +lemma accmethd_Ext [simp]: 
   1.762 +  "accmethd tprg S Ext = methd tprg Ext"
   1.763 +apply (simp add: accmethd_def)
   1.764 +apply (rule filter_tab_all_True)
   1.765 +apply (auto simp add: snd_special_simp fst_special_simp)
   1.766 +done
   1.767 +
   1.768 +(* ### Weiter hoch *)
   1.769 +lemma cls_Ext: "class tprg Ext = Some ExtCl"
   1.770 +by simp
   1.771 +lemma dynmethd_Ext_foo:
   1.772 + "dynmethd tprg Base Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
   1.773 +  = Some (Ext,snd Ext_foo)"
   1.774 +proof -
   1.775 +  have "methd tprg Base \<lparr>name = foo, parTs = [Class Base]\<rparr> 
   1.776 +          = Some (Base,snd Base_foo)" and
   1.777 +       "methd tprg Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> 
   1.778 +          = Some (Ext,snd Ext_foo)" 
   1.779 +    by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def)
   1.780 +  with cls_Ext ws_tprg Ext_foo_overrides_Base_foo
   1.781 +  show ?thesis
   1.782 +    by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def)
   1.783 +qed
   1.784 +
   1.785 +lemma Base_fields_accessible[simp]:
   1.786 + "accfield tprg S Base 
   1.787 +  = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))"
   1.788 +apply (auto simp add: accfield_def expand_fun_eq Let_def 
   1.789 +                      accessible_in_RefT_simp
   1.790 +                      is_public_def
   1.791 +                      BaseCl_def
   1.792 +                      permits_acc_def
   1.793 +                      declared_in_def 
   1.794 +                      cdeclaredfield_def
   1.795 +               intro!: filter_tab_all_True_Some filter_tab_None
   1.796 +                       accessible_fromR.immediate
   1.797 +               intro: members.Immediate)
   1.798 +done
   1.799 +
   1.800 +
   1.801 +lemma arr_member_of_Base:
   1.802 +  "tprg\<turnstile>(Base, fdecl (arr, 
   1.803 +                 \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
   1.804 +          member_of Base"
   1.805 +by (auto intro: members.Immediate 
   1.806 +       simp add: declared_in_def cdeclaredfield_def BaseCl_def)
   1.807 + 
   1.808 +lemma arr_member_of_Ext:
   1.809 +  "tprg\<turnstile>(Base, fdecl (arr, 
   1.810 +                    \<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>))
   1.811 +             member_of Ext"
   1.812 +apply (rule members.Inherited)
   1.813 +apply   (simp add: inheritable_in_def)
   1.814 +apply   (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def)
   1.815 +apply   (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def)
   1.816 +done
   1.817 +
   1.818 +lemma Ext_fields_accessible[simp]:
   1.819 +"accfield tprg S Ext 
   1.820 +  = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))"
   1.821 +apply (auto simp add: accfield_def expand_fun_eq Let_def 
   1.822 +                      accessible_in_RefT_simp
   1.823 +                      is_public_def
   1.824 +                      BaseCl_def
   1.825 +                      ExtCl_def
   1.826 +                      permits_acc_def
   1.827 +               intro!: filter_tab_all_True_Some filter_tab_None
   1.828 +                       accessible_fromR.immediate)
   1.829 +apply (auto intro: members.Immediate arr_member_of_Ext
   1.830 +            simp add: declared_in_def cdeclaredfield_def ExtCl_def)
   1.831 +done
   1.832 +
   1.833 +lemma array_of_PrimT_acc [simp]:
   1.834 + "is_acc_type tprg java_lang (PrimT t.[])"
   1.835 +apply (simp add: is_acc_type_def accessible_in_RefT_simp)
   1.836 +done
   1.837 +
   1.838 +lemma PrimT_acc [simp]: 
   1.839 + "is_acc_type tprg java_lang (PrimT t)"
   1.840 +apply (simp add: is_acc_type_def accessible_in_RefT_simp)
   1.841 +done
   1.842 +
   1.843 +lemma Object_acc [simp]:
   1.844 + "is_acc_class tprg java_lang Object"
   1.845 +apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def)
   1.846 +done
   1.847 +
   1.848 +
   1.849 +section "well-formedness"
   1.850 +
   1.851 +
   1.852 +lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)"
   1.853 +apply (unfold wf_idecl_def HasFooInt_def)
   1.854 +apply (auto intro!: wf_mheadI ws_idecl_HasFoo 
   1.855 +            simp add: foo_sig_def foo_mhead_def mhead_resTy_simp
   1.856 +                      member_is_static_simp )
   1.857 +done
   1.858 +
   1.859 +declare wt.Skip [rule del] wt.Init [rule del]
   1.860 +lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def
   1.861 +lemmas Ext_foo_defs  = Ext_foo_def  foo_sig_def
   1.862 +ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *}
   1.863 +lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros
   1.864 +
   1.865 +lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo"
   1.866 +apply (unfold Base_foo_defs )
   1.867 +apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs
   1.868 +            simp add: mhead_resTy_simp)
   1.869 +done
   1.870 +
   1.871 +lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo"
   1.872 +apply (unfold Ext_foo_defs )
   1.873 +apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs 
   1.874 +            simp add: mhead_resTy_simp )
   1.875 +apply  (rule wt.Cast)
   1.876 +prefer 2
   1.877 +apply    simp
   1.878 +apply   (rule_tac [2] narrow.subcls [THEN cast.narrow])
   1.879 +apply   (auto intro!: wtIs)
   1.880 +done
   1.881 +
   1.882 +declare mhead_resTy_simp [simp add]
   1.883 +declare member_is_static_simp [simp add]
   1.884 +
   1.885 +lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)"
   1.886 +apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def)
   1.887 +apply (auto intro!: wf_Base_foo)
   1.888 +apply       (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def)
   1.889 +apply (auto intro!: wtIs)
   1.890 +apply (auto simp add: Base_foo_defs entails_def Let_def)
   1.891 +apply   (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+
   1.892 +apply   (insert Base_foo_no_hide         , simp add: Base_foo_def,blast)
   1.893 +done
   1.894 +
   1.895 +
   1.896 +lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)"
   1.897 +apply (unfold wf_cdecl_def ExtCl_def)
   1.898 +apply (auto intro!: wf_Ext_foo ws_cdecl_Ext)
   1.899 +apply (auto simp add: entails_def snd_special_simp)
   1.900 +apply (insert Ext_foo_stat_override)
   1.901 +apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   1.902 +apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   1.903 +apply  (force simp add: qmdecl_def Ext_foo_def Base_foo_def)
   1.904 +apply (insert Ext_foo_no_hide)
   1.905 +apply  (simp_all add: qmdecl_def)
   1.906 +apply  blast+
   1.907 +done
   1.908 +
   1.909 +lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)"
   1.910 +apply (simp (no_asm) add: Ifaces_def)
   1.911 +apply (simp (no_asm_simp))
   1.912 +apply (rule wf_HasFoo)
   1.913 +done
   1.914 +
   1.915 +lemma wf_cdecl_all_standard_classes: 
   1.916 +  "Ball (set standard_classes) (wf_cdecl tprg)"
   1.917 +apply (unfold standard_classes_def Let_def 
   1.918 +       ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
   1.919 +apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
   1.920 +apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def)
   1.921 +apply (auto simp add: Object_def Classes_def standard_classes_def 
   1.922 +                      SXcptC_def SXcpt_def)
   1.923 +done
   1.924 +
   1.925 +lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)"
   1.926 +apply (simp (no_asm) add: Classes_def)
   1.927 +apply (simp (no_asm_simp))
   1.928 +apply   (rule wf_BaseC [THEN conjI])
   1.929 +apply  (rule wf_ExtC [THEN conjI])
   1.930 +apply (rule wf_cdecl_all_standard_classes)
   1.931 +done
   1.932 +
   1.933 +theorem wf_tprg: "wf_prog tprg"
   1.934 +apply (unfold wf_prog_def Let_def)
   1.935 +apply (simp (no_asm) add: unique_ifaces unique_classes)
   1.936 +apply (rule conjI)
   1.937 +apply  ((simp (no_asm) add: Classes_def standard_classes_def))
   1.938 +apply (rule conjI)
   1.939 +apply (simp add: Object_mdecls_def)
   1.940 +apply safe
   1.941 +apply  (cut_tac xn_cases_old)   (* FIXME (insert xn_cases) *)
   1.942 +apply  (simp (no_asm_simp) add: Classes_def standard_classes_def)
   1.943 +apply  (insert wf_idecl_all)
   1.944 +apply  (insert wf_cdecl_all)
   1.945 +apply  auto
   1.946 +done
   1.947 +
   1.948 +
   1.949 +section "max spec"
   1.950 +
   1.951 +lemma appl_methds_Base_foo: 
   1.952 +"appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> =  
   1.953 +  {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
   1.954 +    ,[Class Base])}"
   1.955 +apply (unfold appl_methds_def)
   1.956 +apply (simp (no_asm))
   1.957 +apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base")
   1.958 +apply  (auto simp add: cmheads_def Base_foo_defs)
   1.959 +done
   1.960 +
   1.961 +lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = 
   1.962 +  {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>)
   1.963 +   , [Class Base])}"
   1.964 +apply (unfold max_spec_def)
   1.965 +apply (simp (no_asm) add: appl_methds_Base_foo)
   1.966 +apply auto
   1.967 +done
   1.968 +
   1.969 +
   1.970 +section "well-typedness"
   1.971 +
   1.972 +lemma wt_test: "\<lparr>prg=tprg,cls=S,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>"
   1.973 +apply (unfold test_def arr_viewed_from_def)
   1.974 +(* ?pTs = [Class Base] *)
   1.975 +apply (rule wtIs (* ;; *))
   1.976 +apply  (rule wtIs (* Ass *))
   1.977 +apply  (rule wtIs (* NewC *))
   1.978 +apply     (rule wtIs (* LVar *))
   1.979 +apply      (simp)
   1.980 +apply     (simp)
   1.981 +apply    (simp)
   1.982 +apply   (rule wtIs (* NewC *))
   1.983 +apply   (simp)
   1.984 +apply  (simp)
   1.985 +apply (rule wtIs (* Try *))
   1.986 +prefer 4
   1.987 +apply    (simp)
   1.988 +defer
   1.989 +apply    (rule wtIs (* Expr *))
   1.990 +apply    (rule wtIs (* Call *))
   1.991 +apply       (rule wtIs (* Acc *))
   1.992 +apply       (rule wtIs (* LVar *))
   1.993 +apply        (simp)
   1.994 +apply       (simp)
   1.995 +apply      (rule wtIs (* Cons *))
   1.996 +apply       (rule wtIs (* Lit *))
   1.997 +apply       (simp)
   1.998 +apply      (rule wtIs (* Nil *))
   1.999 +apply     (simp)
  1.1000 +apply     (rule max_spec_Base_foo)
  1.1001 +apply    (simp)
  1.1002 +apply   (simp)
  1.1003 +apply  (simp)
  1.1004 +apply  (simp)
  1.1005 +apply (rule wtIs (* While *))
  1.1006 +apply  (rule wtIs (* Acc *))
  1.1007 +apply   (rule wtIs (* AVar *))
  1.1008 +apply   (rule wtIs (* Acc *))
  1.1009 +apply   (rule wtIs (* FVar *))
  1.1010 +apply    (rule wtIs (* StatRef *))
  1.1011 +apply    (simp)
  1.1012 +apply   (simp)
  1.1013 +apply   (simp )
  1.1014 +apply   (simp)
  1.1015 +apply  (rule wtIs (* LVar *))
  1.1016 +apply  (simp)
  1.1017 +apply (rule wtIs (* Skip *))
  1.1018 +done
  1.1019 +
  1.1020 +
  1.1021 +section "execution"
  1.1022 +
  1.1023 +lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow>  
  1.1024 +  new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n"
  1.1025 +apply (frule atleast_free_SucD)
  1.1026 +apply (drule atleast_free_Suc [THEN iffD1])
  1.1027 +apply clarsimp
  1.1028 +apply (frule new_Addr_SomeI)
  1.1029 +apply force
  1.1030 +done
  1.1031 +
  1.1032 +declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp]
  1.1033 +declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp]
  1.1034 +declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp]
  1.1035 +        Base_foo_defs  [simp]
  1.1036 +
  1.1037 +ML {* bind_thms ("eval_intros", map 
  1.1038 +        (simplify (simpset() delsimps [thm "Skip_eq"]
  1.1039 +                             addsimps [thm "lvar_def"]) o 
  1.1040 +         rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *}
  1.1041 +lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros
  1.1042 +
  1.1043 +consts
  1.1044 +  a :: loc
  1.1045 +  b :: loc
  1.1046 +  c :: loc
  1.1047 +  
  1.1048 +syntax
  1.1049 +
  1.1050 +  tprg :: prog
  1.1051 +
  1.1052 +  obj_a :: obj
  1.1053 +  obj_b :: obj
  1.1054 +  obj_c :: obj
  1.1055 +  arr_N :: "(vn, val) table"
  1.1056 +  arr_a :: "(vn, val) table"
  1.1057 +  globs1 :: globs
  1.1058 +  globs2 :: globs
  1.1059 +  globs3 :: globs
  1.1060 +  globs8 :: globs
  1.1061 +  locs3 :: locals
  1.1062 +  locs4 :: locals
  1.1063 +  locs8 :: locals
  1.1064 +  s0  :: state
  1.1065 +  s0' :: state
  1.1066 +  s9' :: state
  1.1067 +  s1  :: state
  1.1068 +  s1' :: state
  1.1069 +  s2  :: state
  1.1070 +  s2' :: state
  1.1071 +  s3  :: state
  1.1072 +  s3' :: state
  1.1073 +  s4  :: state
  1.1074 +  s4' :: state
  1.1075 +  s6' :: state
  1.1076 +  s7' :: state
  1.1077 +  s8  :: state
  1.1078 +  s8' :: state
  1.1079 +
  1.1080 +translations
  1.1081 +
  1.1082 +  "tprg"    == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>"
  1.1083 +  
  1.1084 +  "obj_a"   <= "\<lparr>tag=Arr (PrimT Boolean) two
  1.1085 +                ,values=empty(Inr 0\<mapsto>Bool False)(Inr one\<mapsto>Bool False)\<rparr>"
  1.1086 +  "obj_b"   <= "\<lparr>tag=CInst Ext
  1.1087 +                ,values=(empty(Inl (vee, Base)\<mapsto>Null   ) 
  1.1088 +			      (Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>"
  1.1089 +  "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=empty\<rparr>"
  1.1090 +  "arr_N"   == "empty(Inl (arr, Base)\<mapsto>Null)"
  1.1091 +  "arr_a"   == "empty(Inl (arr, Base)\<mapsto>Addr a)"
  1.1092 +  "globs1"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
  1.1093 +		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
  1.1094 +		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)"
  1.1095 +  "globs2"  == "empty(Inr Ext   \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
  1.1096 +		     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)
  1.1097 +		     (Inl a\<mapsto>obj_a)
  1.1098 +		     (Inr Base  \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
  1.1099 +  "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
  1.1100 +  "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
  1.1101 +  "locs3"   == "empty(VName e\<mapsto>Addr b)"
  1.1102 +  "locs4"   == "empty(VName z\<mapsto>Null)(Inr()\<mapsto>Addr b)"
  1.1103 +  "locs8"   == "locs3(VName z\<mapsto>Addr c)"
  1.1104 +  "s0"  == "       st empty  empty"
  1.1105 +  "s0'" == " Norm  s0"
  1.1106 +  "s1"  == "       st globs1 empty"
  1.1107 +  "s1'" == " Norm  s1"
  1.1108 +  "s2"  == "       st globs2 empty"
  1.1109 +  "s2'" == " Norm  s2"
  1.1110 +  "s3"  == "       st globs3 locs3 "
  1.1111 +  "s3'" == " Norm  s3"
  1.1112 +  "s4"  == "       st globs3 locs4"
  1.1113 +  "s4'" == " Norm  s4"
  1.1114 +  "s6'" == "(Some (Xcpt (Std NullPointer)), s4)"
  1.1115 +  "s7'" == "(Some (Xcpt (Std NullPointer)), s3)"
  1.1116 +  "s8"  == "       st globs8 locs8"
  1.1117 +  "s8'" == " Norm  s8"
  1.1118 +  "s9'" == "(Some (Xcpt (Std IndOutBound)), s8)"
  1.1119 +
  1.1120 +
  1.1121 +syntax "four"::nat
  1.1122 +       "tree"::nat
  1.1123 +       "two" ::nat
  1.1124 +       "one" ::nat
  1.1125 +translations 
  1.1126 +  "one"  == "Suc 0"
  1.1127 +  "two"  == "Suc one"
  1.1128 +  "tree" == "Suc two"
  1.1129 +  "four" == "Suc tree"
  1.1130 +
  1.1131 +declare Pair_eq [simp del]
  1.1132 +lemma exec_test: 
  1.1133 +"\<lbrakk>the (new_Addr (heap  s1)) = a;  
  1.1134 +  the (new_Addr (heap ?s2)) = b;  
  1.1135 +  the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow>  
  1.1136 +  atleast_free  (heap s0) four \<Longrightarrow>  
  1.1137 +  tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'"
  1.1138 +apply (unfold test_def arr_viewed_from_def)
  1.1139 +(* ?s9' = s9' *)
  1.1140 +apply (simp (no_asm_use))
  1.1141 +apply (drule (1) alloc_one,clarsimp)
  1.1142 +apply (rule eval_Is (* ;; *))
  1.1143 +apply  (erule_tac V = "the (new_Addr ?h) = c" in thin_rl)
  1.1144 +apply  (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
  1.1145 +apply  (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
  1.1146 +apply  (rule eval_Is (* Expr *))
  1.1147 +apply  (rule eval_Is (* Ass *))
  1.1148 +apply   (rule eval_Is (* LVar *))
  1.1149 +apply  (rule eval_Is (* NewC *))
  1.1150 +      (* begin init Ext *)
  1.1151 +apply   (erule_tac V = "the (new_Addr ?h) = b" in thin_rl)
  1.1152 +apply   (erule_tac V = "atleast_free ?h tree" in thin_rl)
  1.1153 +apply   (erule_tac [2] V = "atleast_free ?h four" in thin_rl)
  1.1154 +apply   (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl)
  1.1155 +apply   (rule eval_Is (* Init Ext *))
  1.1156 +apply   (simp)
  1.1157 +apply   (rule conjI)
  1.1158 +prefer 2 apply (rule conjI HOL.refl)+
  1.1159 +apply   (rule eval_Is (* Init Base *))
  1.1160 +apply   (simp add: arr_viewed_from_def)
  1.1161 +apply   (rule conjI)
  1.1162 +apply    (rule eval_Is (* Init Object *))
  1.1163 +apply    (simp)
  1.1164 +apply    (rule conjI, rule HOL.refl)+
  1.1165 +apply    (rule HOL.refl)
  1.1166 +apply   (simp)
  1.1167 +apply   (rule conjI, rule_tac [2] HOL.refl)
  1.1168 +apply   (rule eval_Is (* Expr *))
  1.1169 +apply   (rule eval_Is (* Ass *))
  1.1170 +apply    (rule eval_Is (* FVar *))
  1.1171 +apply      (rule init_done, simp)
  1.1172 +apply     (rule eval_Is (* StatRef *))
  1.1173 +apply    (simp)
  1.1174 +apply   (rule eval_Is (* NewA *))
  1.1175 +apply     (simp)
  1.1176 +apply    (rule eval_Is (* Lit *))
  1.1177 +apply   (simp)
  1.1178 +apply   (rule halloc.New)
  1.1179 +apply    (simp (no_asm_simp))
  1.1180 +apply   (drule atleast_free_weaken,rotate_tac -1,drule atleast_free_weaken)
  1.1181 +apply   (simp (no_asm_simp))
  1.1182 +apply  (simp add: upd_gobj_def)
  1.1183 +      (* end init Ext *)
  1.1184 +apply  (rule halloc.New)
  1.1185 +apply   (drule alloc_one)
  1.1186 +prefer 2 apply fast
  1.1187 +apply   (simp (no_asm_simp))
  1.1188 +apply  (drule atleast_free_weaken)
  1.1189 +apply  force
  1.1190 +apply (simp)
  1.1191 +apply (drule alloc_one)
  1.1192 +apply  (simp (no_asm_simp))
  1.1193 +apply clarsimp
  1.1194 +apply (erule_tac V = "atleast_free ?h tree" in thin_rl)
  1.1195 +apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
  1.1196 +apply (simp (no_asm_use))
  1.1197 +apply (rule eval_Is (* Try *))
  1.1198 +apply   (rule eval_Is (* Expr *))
  1.1199 +      (* begin method call *)
  1.1200 +apply   (rule eval_Is (* Call *))
  1.1201 +apply      (rule eval_Is (* Acc *))
  1.1202 +apply      (rule eval_Is (* LVar *))
  1.1203 +apply     (rule eval_Is (* Cons *))
  1.1204 +apply      (rule eval_Is (* Lit *))
  1.1205 +apply     (rule eval_Is (* Nil *))
  1.1206 +apply    (simp)
  1.1207 +apply   (simp)
  1.1208 +apply   (rule eval_Is (* Methd *))
  1.1209 +apply   (simp add: body_def Let_def)
  1.1210 +apply   (rule eval_Is (* Body *))
  1.1211 +apply     (rule init_done, simp)
  1.1212 +apply       (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
  1.1213 +apply    (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo)
  1.1214 +apply    (rule eval_Is (* Expr *))
  1.1215 +apply    (rule eval_Is (* Ass *))
  1.1216 +apply     (rule eval_Is (* FVar *))
  1.1217 +apply       (rule init_done, simp)
  1.1218 +apply      (rule eval_Is (* Cast *))
  1.1219 +apply       (rule eval_Is (* Acc *))
  1.1220 +apply       (rule eval_Is (* LVar *))
  1.1221 +apply      (simp)
  1.1222 +apply     (simp split del: split_if)
  1.1223 +apply    (rule eval_Is (* XcptE *))
  1.1224 +apply   (simp)
  1.1225 +      (* end method call *)
  1.1226 +apply  (rule sxalloc.intros)
  1.1227 +apply  (rule halloc.New)
  1.1228 +apply   (erule alloc_one [THEN conjunct1])
  1.1229 +apply   (simp (no_asm_simp))
  1.1230 +apply  (simp (no_asm_simp))
  1.1231 +apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if)
  1.1232 +apply (drule alloc_one [THEN conjunct1])
  1.1233 +apply  (simp (no_asm_simp))
  1.1234 +apply (erule_tac V = "atleast_free ?h two" in thin_rl)
  1.1235 +apply (drule_tac x = "a" in new_AddrD2 [THEN spec])
  1.1236 +apply simp
  1.1237 +apply (rule eval_Is (* While *))
  1.1238 +apply  (rule eval_Is (* Acc *))
  1.1239 +apply  (rule eval_Is (* AVar *))
  1.1240 +apply    (rule eval_Is (* Acc *))
  1.1241 +apply    (rule eval_Is (* FVar *))
  1.1242 +apply      (rule init_done, simp)
  1.1243 +apply     (rule eval_Is (* StatRef *))
  1.1244 +apply    (simp)
  1.1245 +apply   (rule eval_Is (* Lit *))
  1.1246 +apply  (simp (no_asm_simp))
  1.1247 +apply (auto simp add: in_bounds_def)
  1.1248 +done
  1.1249 +declare Pair_eq [simp]
  1.1250 +
  1.1251 +end