src/HOL/MicroJava/J/Example.thy
author wenzelm
Fri Apr 23 23:35:43 2010 +0200 (2010-04-23)
changeset 36319 8feb2c4bef1a
parent 35102 cc7a0b9f938c
child 45605 a89b4bc311a5
permissions -rwxr-xr-x
mark schematic statements explicitly;
     1 (*  Title:      HOL/MicroJava/J/Example.thy
     2     Author:     David von Oheimb
     3     Copyright   1999 Technische Universitaet Muenchen
     4 *)
     5 
     6 header {* \isaheader{Example MicroJava Program} *}
     7 
     8 theory Example imports SystemClasses Eval begin
     9 
    10 text {* 
    11 The following example MicroJava program includes:
    12  class declarations with inheritance, hiding of fields, and overriding of
    13   methods (with refined result type), 
    14  instance creation, local assignment, sequential composition,
    15  method call with dynamic binding, literal values,
    16  expression statement, local access, type cast, field assignment (in part), 
    17  skip.
    18 
    19 \begin{verbatim}
    20 class Base {
    21   boolean vee;
    22   Base foo(Base x) {return x;}
    23 }
    24 
    25 class Ext extends Base {
    26   int vee;
    27   Ext foo(Base x) {((Ext)x).vee=1; return null;}
    28 }
    29 
    30 class Example {
    31   public static void main (String args[]) {
    32     Base e=new Ext();
    33     e.foo(null);
    34   }
    35 }
    36 \end{verbatim}
    37 *}
    38 
    39 datatype cnam' = Base' | Ext'
    40 datatype vnam' = vee' | x' | e'
    41 
    42 consts
    43   cnam' :: "cnam' => cname"
    44   vnam' :: "vnam' => vnam"
    45 
    46 -- "@{text cnam'} and @{text vnam'} are intended to be isomorphic 
    47     to @{text cnam} and @{text vnam}"
    48 axioms 
    49   inj_cnam':  "(cnam' x = cnam' y) = (x = y)"
    50   inj_vnam':  "(vnam' x = vnam' y) = (x = y)"
    51 
    52   surj_cnam': "\<exists>m. n = cnam' m"
    53   surj_vnam': "\<exists>m. n = vnam' m"
    54 
    55 declare inj_cnam' [simp] inj_vnam' [simp]
    56 
    57 abbreviation Base :: cname
    58   where "Base == cnam' Base'"
    59 abbreviation Ext :: cname
    60   where "Ext == cnam' Ext'"
    61 abbreviation vee :: vname
    62   where "vee == VName (vnam' vee')"
    63 abbreviation x :: vname
    64   where "x == VName (vnam' x')"
    65 abbreviation e :: vname
    66   where "e == VName (vnam' e')"
    67 
    68 axioms
    69   Base_not_Object: "Base \<noteq> Object"
    70   Ext_not_Object:  "Ext  \<noteq> Object"
    71   Base_not_Xcpt:   "Base \<noteq> Xcpt z"
    72   Ext_not_Xcpt:    "Ext  \<noteq> Xcpt z"
    73   e_not_This:      "e \<noteq> This"  
    74 
    75 declare Base_not_Object [simp] Ext_not_Object [simp]
    76 declare Base_not_Xcpt [simp] Ext_not_Xcpt [simp]
    77 declare e_not_This [simp]
    78 declare Base_not_Object [symmetric, simp]
    79 declare Ext_not_Object  [symmetric, simp]
    80 declare Base_not_Xcpt [symmetric, simp]
    81 declare Ext_not_Xcpt  [symmetric, simp]
    82 
    83 consts
    84   foo_Base::  java_mb
    85   foo_Ext ::  java_mb
    86   BaseC   :: "java_mb cdecl"
    87   ExtC    :: "java_mb cdecl"
    88   test    ::  stmt
    89   foo   ::  mname
    90   a   ::  loc
    91   b       ::  loc
    92 
    93 defs
    94   foo_Base_def:"foo_Base == ([x],[],Skip,LAcc x)"
    95   BaseC_def:"BaseC == (Base, (Object, 
    96            [(vee, PrimT Boolean)], 
    97            [((foo,[Class Base]),Class Base,foo_Base)]))"
    98   foo_Ext_def:"foo_Ext == ([x],[],Expr( {Ext}Cast Ext
    99                (LAcc x)..vee:=Lit (Intg Numeral1)),
   100            Lit Null)"
   101   ExtC_def: "ExtC  == (Ext,  (Base  , 
   102            [(vee, PrimT Integer)], 
   103            [((foo,[Class Base]),Class Ext,foo_Ext)]))"
   104 
   105   test_def:"test == Expr(e::=NewC Ext);; 
   106                     Expr({Base}LAcc e..foo({[Class Base]}[Lit Null]))"
   107 
   108 
   109 abbreviation
   110   NP  :: xcpt where
   111   "NP == NullPointer"
   112 
   113 abbreviation
   114   tprg  ::"java_mb prog" where
   115   "tprg == [ObjectC, BaseC, ExtC, ClassCastC, NullPointerC, OutOfMemoryC]"
   116 
   117 abbreviation
   118   obj1  :: obj where
   119   "obj1 == (Ext, empty((vee, Base)\<mapsto>Bool False) ((vee, Ext )\<mapsto>Intg 0))"
   120 
   121 abbreviation "s0 == Norm    (empty, empty)"
   122 abbreviation "s1 == Norm    (empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
   123 abbreviation "s2 == Norm    (empty(a\<mapsto>obj1),empty(x\<mapsto>Null)(This\<mapsto>Addr a))"
   124 abbreviation "s3 == (Some NP, empty(a\<mapsto>obj1),empty(e\<mapsto>Addr a))"
   125 
   126 lemmas map_of_Cons = map_of.simps(2)
   127 
   128 lemma map_of_Cons1 [simp]: "map_of ((aa,bb)#ps) aa = Some bb"
   129 apply (simp (no_asm))
   130 done
   131 lemma map_of_Cons2 [simp]: "aa\<noteq>k ==> map_of ((k,bb)#ps) aa = map_of ps aa"
   132 apply (simp (no_asm_simp))
   133 done
   134 declare map_of_Cons [simp del] -- "sic!"
   135 
   136 lemma class_tprg_Object [simp]: "class tprg Object = Some (undefined, [], [])"
   137 apply (unfold ObjectC_def class_def)
   138 apply (simp (no_asm))
   139 done
   140 
   141 lemma class_tprg_NP [simp]: "class tprg (Xcpt NP) = Some (Object, [], [])"
   142 apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
   143 apply (simp (no_asm))
   144 done
   145 
   146 lemma class_tprg_OM [simp]: "class tprg (Xcpt OutOfMemory) = Some (Object, [], [])"
   147 apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
   148 apply (simp (no_asm))
   149 done
   150 
   151 lemma class_tprg_CC [simp]: "class tprg (Xcpt ClassCast) = Some (Object, [], [])"
   152 apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
   153 apply (simp (no_asm))
   154 done
   155 
   156 lemma class_tprg_Base [simp]: 
   157 "class tprg Base = Some (Object,  
   158     [(vee, PrimT Boolean)],  
   159           [((foo, [Class Base]), Class Base, foo_Base)])"
   160 apply (unfold ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
   161 apply (simp (no_asm))
   162 done
   163 
   164 lemma class_tprg_Ext [simp]: 
   165 "class tprg Ext = Some (Base,  
   166     [(vee, PrimT Integer)],  
   167           [((foo, [Class Base]), Class Ext, foo_Ext)])"
   168 apply (unfold ObjectC_def BaseC_def ExtC_def class_def)
   169 apply (simp (no_asm))
   170 done
   171 
   172 lemma not_Object_subcls [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ ==> R"
   173 apply (auto dest!: tranclD subcls1D)
   174 done
   175 
   176 lemma subcls_ObjectD [dest!]: "tprg\<turnstile>Object\<preceq>C C ==> C = Object"
   177 apply (erule rtrancl_induct)
   178 apply  auto
   179 apply (drule subcls1D)
   180 apply auto
   181 done
   182 
   183 lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+  ==> R"
   184 apply (auto dest!: tranclD subcls1D)
   185 done
   186 
   187 lemma class_tprgD: 
   188 "class tprg C = Some z ==> C=Object \<or> C=Base \<or> C=Ext \<or> C=Xcpt NP \<or> C=Xcpt ClassCast \<or> C=Xcpt OutOfMemory"
   189 apply (unfold ObjectC_def ClassCastC_def NullPointerC_def OutOfMemoryC_def BaseC_def ExtC_def class_def)
   190 apply (auto split add: split_if_asm simp add: map_of_Cons)
   191 done
   192 
   193 lemma not_class_subcls_class [elim!]: "(C, C) \<in> (subcls1 tprg)^+ ==> R"
   194 apply (auto dest!: tranclD subcls1D)
   195 apply (frule class_tprgD)
   196 apply (auto dest!:)
   197 apply (drule rtranclD)
   198 apply auto
   199 done
   200 
   201 lemma unique_classes: "unique tprg"
   202 apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
   203 done
   204 
   205 lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"], standard]
   206 
   207 lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
   208 apply (rule subcls_direct)
   209 apply auto
   210 done
   211 
   212 lemma Ext_widen_Base [simp]: "tprg\<turnstile>Class Ext\<preceq> Class Base"
   213 apply (rule widen.subcls)
   214 apply (simp (no_asm))
   215 done
   216 
   217 declare ty_expr_ty_exprs_wt_stmt.intros [intro!]
   218 
   219 lemma acyclic_subcls1': "acyclic (subcls1 tprg)"
   220 apply (rule acyclicI)
   221 apply safe
   222 done
   223 
   224 lemmas wf_subcls1' = acyclic_subcls1' [THEN finite_subcls1 [THEN finite_acyclic_wf_converse]]
   225 
   226 lemmas fields_rec' = wf_subcls1' [THEN [2] fields_rec_lemma]
   227 
   228 lemma fields_Object [simp]: "fields (tprg, Object) = []"
   229 apply (subst fields_rec')
   230 apply   auto
   231 done
   232 
   233 declare is_class_def [simp]
   234 
   235 lemma fields_Base [simp]: "fields (tprg,Base) = [((vee, Base), PrimT Boolean)]"
   236 apply (subst fields_rec')
   237 apply   auto
   238 done
   239 
   240 lemma fields_Ext [simp]: 
   241   "fields (tprg, Ext)  = [((vee, Ext ), PrimT Integer)] @ fields (tprg, Base)"
   242 apply (rule trans)
   243 apply  (rule fields_rec')
   244 apply   auto
   245 done
   246 
   247 lemmas method_rec' = wf_subcls1' [THEN [2] method_rec_lemma]
   248 
   249 lemma method_Object [simp]: "method (tprg,Object) = map_of []"
   250 apply (subst method_rec')
   251 apply  auto
   252 done
   253 
   254 lemma method_Base [simp]: "method (tprg, Base) = map_of  
   255   [((foo, [Class Base]), Base, (Class Base, foo_Base))]"
   256 apply (rule trans)
   257 apply  (rule method_rec')
   258 apply  auto
   259 done
   260 
   261 lemma method_Ext [simp]: "method (tprg, Ext) = (method (tprg, Base) ++ map_of  
   262   [((foo, [Class Base]), Ext , (Class Ext, foo_Ext))])"
   263 apply (rule trans)
   264 apply  (rule method_rec')
   265 apply  auto
   266 done
   267 
   268 lemma wf_foo_Base: 
   269 "wf_mdecl wf_java_mdecl tprg Base ((foo, [Class Base]), (Class Base, foo_Base))"
   270 apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Base_def)
   271 apply auto
   272 done
   273 
   274 lemma wf_foo_Ext: 
   275 "wf_mdecl wf_java_mdecl tprg Ext ((foo, [Class Base]), (Class Ext, foo_Ext))"
   276 apply (unfold wf_mdecl_def wf_mhead_def wf_java_mdecl_def foo_Ext_def)
   277 apply auto
   278 apply  (rule ty_expr_ty_exprs_wt_stmt.Cast)
   279 prefer 2
   280 apply   (simp)
   281 apply   (rule_tac [2] cast.subcls)
   282 apply   (unfold field_def)
   283 apply   auto
   284 done
   285 
   286 lemma wf_ObjectC: 
   287 "ws_cdecl tprg ObjectC \<and> 
   288   wf_cdecl_mdecl wf_java_mdecl tprg ObjectC \<and> wf_mrT tprg ObjectC"
   289 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
   290   wf_mrT_def wf_fdecl_def ObjectC_def)
   291 apply (simp (no_asm))
   292 done
   293 
   294 lemma wf_NP:
   295 "ws_cdecl tprg NullPointerC \<and>
   296   wf_cdecl_mdecl wf_java_mdecl tprg NullPointerC \<and> wf_mrT tprg NullPointerC"
   297 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
   298   wf_mrT_def wf_fdecl_def NullPointerC_def)
   299 apply (simp add: class_def)
   300 apply (fold NullPointerC_def class_def)
   301 apply auto
   302 done
   303 
   304 lemma wf_OM:
   305 "ws_cdecl tprg OutOfMemoryC \<and>
   306   wf_cdecl_mdecl wf_java_mdecl tprg OutOfMemoryC \<and> wf_mrT tprg OutOfMemoryC"
   307 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
   308   wf_mrT_def wf_fdecl_def OutOfMemoryC_def)
   309 apply (simp add: class_def)
   310 apply (fold OutOfMemoryC_def class_def)
   311 apply auto
   312 done
   313 
   314 lemma wf_CC:
   315 "ws_cdecl tprg ClassCastC \<and>
   316   wf_cdecl_mdecl wf_java_mdecl tprg ClassCastC \<and> wf_mrT tprg ClassCastC"
   317 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def 
   318   wf_mrT_def wf_fdecl_def ClassCastC_def)
   319 apply (simp add: class_def)
   320 apply (fold ClassCastC_def class_def)
   321 apply auto
   322 done
   323 
   324 lemma wf_BaseC: 
   325 "ws_cdecl tprg BaseC \<and>
   326   wf_cdecl_mdecl wf_java_mdecl tprg BaseC \<and> wf_mrT tprg BaseC"
   327 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
   328   wf_mrT_def wf_fdecl_def BaseC_def)
   329 apply (simp (no_asm))
   330 apply (fold BaseC_def)
   331 apply (rule mp) defer apply (rule wf_foo_Base)
   332 apply (auto simp add: wf_mdecl_def)
   333 done
   334 
   335 
   336 lemma wf_ExtC: 
   337 "ws_cdecl tprg ExtC \<and>
   338   wf_cdecl_mdecl wf_java_mdecl tprg ExtC \<and> wf_mrT tprg ExtC"
   339 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def
   340   wf_mrT_def wf_fdecl_def ExtC_def)
   341 apply (simp (no_asm))
   342 apply (fold ExtC_def)
   343 apply (rule mp) defer apply (rule wf_foo_Ext)
   344 apply (auto simp add: wf_mdecl_def)
   345 apply (drule rtranclD)
   346 apply auto
   347 done
   348 
   349 
   350 lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def)
   351 
   352 lemma wf_tprg: 
   353 "wf_prog wf_java_mdecl tprg"
   354 apply (unfold wf_prog_def ws_prog_def Let_def)
   355 apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes)
   356 apply (rule wf_syscls)
   357 apply (simp add: SystemClasses_def)
   358 done
   359 
   360 lemma appl_methds_foo_Base: 
   361 "appl_methds tprg Base (foo, [NT]) =  
   362   {((Class Base, Class Base), [Class Base])}"
   363 apply (unfold appl_methds_def)
   364 apply (simp (no_asm))
   365 done
   366 
   367 lemma max_spec_foo_Base: "max_spec tprg Base (foo, [NT]) =  
   368   {((Class Base, Class Base), [Class Base])}"
   369 apply (unfold max_spec_def)
   370 apply (auto simp add: appl_methds_foo_Base)
   371 done
   372 
   373 ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *}
   374 schematic_lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>  
   375   Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
   376 apply (tactic t) -- ";;"
   377 apply  (tactic t) -- "Expr"
   378 apply  (tactic t) -- "LAss"
   379 apply    simp -- {* @{text "e \<noteq> This"} *}
   380 apply    (tactic t) -- "LAcc"
   381 apply     (simp (no_asm))
   382 apply    (simp (no_asm))
   383 apply   (tactic t) -- "NewC"
   384 apply   (simp (no_asm))
   385 apply  (simp (no_asm))
   386 apply (tactic t) -- "Expr"
   387 apply (tactic t) -- "Call"
   388 apply   (tactic t) -- "LAcc"
   389 apply    (simp (no_asm))
   390 apply   (simp (no_asm))
   391 apply  (tactic t) -- "Cons"
   392 apply   (tactic t) -- "Lit"
   393 apply   (simp (no_asm))
   394 apply  (tactic t) -- "Nil"
   395 apply (simp (no_asm))
   396 apply (rule max_spec_foo_Base)
   397 done
   398 
   399 ML {* val e = resolve_tac (@{thm NewCI} :: @{thms eval_evals_exec.intros}) 1 *}
   400 
   401 declare split_if [split del]
   402 declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
   403 schematic_lemma exec_test: 
   404 " [|new_Addr (heap (snd s0)) = (a, None)|] ==>  
   405   tprg\<turnstile>s0 -test-> ?s"
   406 apply (unfold test_def)
   407 -- "?s = s3 "
   408 apply (tactic e) -- ";;"
   409 apply  (tactic e) -- "Expr"
   410 apply  (tactic e) -- "LAss"
   411 apply   (tactic e) -- "NewC"
   412 apply    force
   413 apply   force
   414 apply  (simp (no_asm))
   415 apply (erule thin_rl)
   416 apply (tactic e) -- "Expr"
   417 apply (tactic e) -- "Call"
   418 apply       (tactic e) -- "LAcc"
   419 apply      force
   420 apply     (tactic e) -- "Cons"
   421 apply      (tactic e) -- "Lit"
   422 apply     (tactic e) -- "Nil"
   423 apply    (simp (no_asm))
   424 apply   (force simp add: foo_Ext_def)
   425 apply  (simp (no_asm))
   426 apply  (tactic e) -- "Expr"
   427 apply  (tactic e) -- "FAss"
   428 apply       (tactic e) -- "Cast"
   429 apply        (tactic e) -- "LAcc"
   430 apply       (simp (no_asm))
   431 apply      (simp (no_asm))
   432 apply     (simp (no_asm))
   433 apply     (tactic e) -- "XcptE"
   434 apply    (simp (no_asm))
   435 apply   (rule surjective_pairing [THEN sym, THEN[2]trans], subst Pair_eq, force)
   436 apply  (simp (no_asm))
   437 apply (simp (no_asm))
   438 apply (tactic e) -- "XcptE"
   439 done
   440 
   441 end