src/HOL/Bali/State.thy
author schirmer
Mon Jan 28 17:00:19 2002 +0100 (2002-01-28)
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
     1 (*  Title:      isabelle/Bali/State.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1997 Technische Universitaet Muenchen
     5 *)
     6 header {* State for evaluation of Java expressions and statements *}
     7 
     8 theory State = DeclConcepts:
     9 
    10 text {*
    11 design issues:
    12 \begin{itemize}
    13 \item all kinds of objects (class instances, arrays, and class objects)
    14   are handeled via a general object abstraction
    15 \item the heap and the map for class objects are combined into a single table
    16   @{text "(recall (loc, obj) table \<times> (qtname, obj) table  ~=  (loc + qtname, obj) table)"}
    17 \end{itemize}
    18 *}
    19 
    20 section "objects"
    21 
    22 datatype  obj_tag =     (* tag for generic object   *)
    23 	  CInst qtname   (* class instance           *)
    24 	| Arr  ty int   (* array with component type and length *)
    25      (* | CStat            the tag is irrelevant for a class object,
    26 			   i.e. the static fields of a class *)
    27 
    28 types	vn   = "fspec + int"                    (* variable name      *)
    29 record	obj  = 
    30           tag :: "obj_tag"                      (* generalized object *)
    31           values :: "(vn, val) table"      
    32 
    33 translations 
    34   "fspec" <= (type) "vname \<times> qtname" 
    35   "vn"    <= (type) "fspec + int"
    36   "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option\<rparr>"
    37   "obj"   <= (type) "\<lparr>tag::obj_tag, values::vn \<Rightarrow> val option,\<dots>::'a\<rparr>"
    38 
    39 constdefs
    40   
    41   the_Arr :: "obj option \<Rightarrow> ty \<times> int \<times> (vn, val) table"
    42  "the_Arr obj \<equiv> \<epsilon>(T,k,t). obj = Some \<lparr>tag=Arr T k,values=t\<rparr>"
    43 
    44 lemma the_Arr_Arr [simp]: "the_Arr (Some \<lparr>tag=Arr T k,values=cs\<rparr>) = (T,k,cs)"
    45 apply (auto simp: the_Arr_def)
    46 done
    47 
    48 lemma the_Arr_Arr1 [simp,intro,dest]:
    49  "\<lbrakk>tag obj = Arr T k\<rbrakk> \<Longrightarrow> the_Arr (Some obj) = (T,k,values obj)"
    50 apply (auto simp add: the_Arr_def)
    51 done
    52 
    53 constdefs
    54 
    55   upd_obj       :: "vn \<Rightarrow> val \<Rightarrow> obj \<Rightarrow> obj" 
    56  "upd_obj n v \<equiv> \<lambda> obj . obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>"
    57 
    58 lemma upd_obj_def2 [simp]: 
    59   "upd_obj n v obj = obj \<lparr>values:=(values obj)(n\<mapsto>v)\<rparr>" 
    60 apply (auto simp: upd_obj_def)
    61 done
    62 
    63 constdefs
    64   obj_ty        :: "obj \<Rightarrow> ty"
    65  "obj_ty obj    \<equiv> case tag obj of 
    66                     CInst C \<Rightarrow> Class C 
    67                   | Arr T k \<Rightarrow> T.[]"
    68 
    69 lemma obj_ty_eq [intro!]: "obj_ty \<lparr>tag=oi,values=x\<rparr> = obj_ty \<lparr>tag=oi,values=y\<rparr>" 
    70 by (simp add: obj_ty_def)
    71 
    72 
    73 lemma obj_ty_eq1 [intro!,dest]: 
    74   "tag obj = tag obj' \<Longrightarrow> obj_ty obj = obj_ty obj'" 
    75 by (simp add: obj_ty_def)
    76 
    77 lemma obj_ty_cong [simp]: 
    78   "obj_ty (obj \<lparr>values:=vs\<rparr>) = obj_ty obj" 
    79 by auto
    80 (*
    81 lemma obj_ty_cong [simp]: 
    82   "obj_ty (obj \<lparr>values:=vs(n\<mapsto>v)\<rparr>) = obj_ty (obj \<lparr>values:=vs\<rparr>)" 
    83 by auto
    84 *)
    85 lemma obj_ty_CInst [simp]: 
    86  "obj_ty \<lparr>tag=CInst C,values=vs\<rparr> = Class C" 
    87 by (simp add: obj_ty_def)
    88 
    89 lemma obj_ty_CInst1 [simp,intro!,dest]: 
    90  "\<lbrakk>tag obj = CInst C\<rbrakk> \<Longrightarrow> obj_ty obj = Class C" 
    91 by (simp add: obj_ty_def)
    92 
    93 lemma obj_ty_Arr [simp]: 
    94  "obj_ty \<lparr>tag=Arr T i,values=vs\<rparr> = T.[]"
    95 by (simp add: obj_ty_def)
    96 
    97 lemma obj_ty_Arr1 [simp,intro!,dest]: 
    98  "\<lbrakk>tag obj = Arr T i\<rbrakk> \<Longrightarrow> obj_ty obj = T.[]"
    99 by (simp add: obj_ty_def)
   100 
   101 lemma obj_ty_widenD: 
   102  "G\<turnstile>obj_ty obj\<preceq>RefT t \<Longrightarrow> (\<exists>C. tag obj = CInst C) \<or> (\<exists>T k. tag obj = Arr T k)"
   103 apply (unfold obj_ty_def)
   104 apply (auto split add: obj_tag.split_asm)
   105 done
   106 
   107 constdefs
   108 
   109   obj_class :: "obj \<Rightarrow> qtname"
   110  "obj_class obj \<equiv> case tag obj of 
   111                     CInst C \<Rightarrow> C 
   112                   | Arr T k \<Rightarrow> Object"
   113 
   114 
   115 lemma obj_class_CInst [simp]: "obj_class \<lparr>tag=CInst C,values=vs\<rparr> = C" 
   116 by (auto simp: obj_class_def)
   117 
   118 lemma obj_class_CInst1 [simp,intro!,dest]: 
   119   "tag obj = CInst C \<Longrightarrow> obj_class obj = C" 
   120 by (auto simp: obj_class_def)
   121 
   122 lemma obj_class_Arr [simp]: "obj_class \<lparr>tag=Arr T k,values=vs\<rparr> = Object" 
   123 by (auto simp: obj_class_def)
   124 
   125 lemma obj_class_Arr1 [simp,intro!,dest]: 
   126  "tag obj = Arr T k \<Longrightarrow> obj_class obj = Object" 
   127 by (auto simp: obj_class_def)
   128 
   129 lemma obj_ty_obj_class: "G\<turnstile>obj_ty obj\<preceq> Class statC = G\<turnstile>obj_class obj \<preceq>\<^sub>C statC"
   130 apply (case_tac "tag obj")
   131 apply (auto simp add: obj_ty_def obj_class_def)
   132 apply (case_tac "statC = Object")
   133 apply (auto dest: widen_Array_Class)
   134 done
   135 
   136 section "object references"
   137 
   138 types oref = "loc + qtname"          (* generalized object reference *)
   139 syntax
   140   Heap  :: "loc   \<Rightarrow> oref"
   141   Stat  :: "qtname \<Rightarrow> oref"
   142 
   143 translations
   144   "Heap" => "Inl"
   145   "Stat" => "Inr"
   146   "oref" <= (type) "loc + qtname"
   147 
   148 constdefs
   149   fields_table::
   150     "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool)  \<Rightarrow> (fspec, ty) table"
   151  "fields_table G C P 
   152     \<equiv> option_map type \<circ> table_of (filter (split P) (DeclConcepts.fields G C))"
   153 
   154 lemma fields_table_SomeI: 
   155 "\<lbrakk>table_of (DeclConcepts.fields G C) n = Some f; P n f\<rbrakk> 
   156  \<Longrightarrow> fields_table G C P n = Some (type f)"
   157 apply (unfold fields_table_def)
   158 apply clarsimp
   159 apply (rule exI)
   160 apply (rule conjI)
   161 apply (erule map_of_filter_in)
   162 apply assumption
   163 apply simp
   164 done
   165 
   166 (* unused *)
   167 lemma fields_table_SomeD': "fields_table G C P fn = Some T \<Longrightarrow>  
   168   \<exists>f. (fn,f)\<in>set(DeclConcepts.fields G C) \<and> type f = T"
   169 apply (unfold fields_table_def)
   170 apply clarsimp
   171 apply (drule map_of_SomeD)
   172 apply auto
   173 done
   174 
   175 lemma fields_table_SomeD: 
   176 "\<lbrakk>fields_table G C P fn = Some T; unique (DeclConcepts.fields G C)\<rbrakk> \<Longrightarrow>  
   177   \<exists>f. table_of (DeclConcepts.fields G C) fn = Some f \<and> type f = T"
   178 apply (unfold fields_table_def)
   179 apply clarsimp
   180 apply (rule exI)
   181 apply (rule conjI)
   182 apply (erule table_of_filter_unique_SomeD)
   183 apply assumption
   184 apply simp
   185 done
   186 
   187 constdefs
   188   in_bounds :: "int \<Rightarrow> int \<Rightarrow> bool"            ("(_/ in'_bounds _)" [50, 51] 50)
   189  "i in_bounds k \<equiv> 0 \<le> i \<and> i < k"
   190 
   191   arr_comps :: "'a \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a option"
   192  "arr_comps T k \<equiv> \<lambda>i. if i in_bounds k then Some T else None"
   193   
   194   var_tys       :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> (vn, ty) table"
   195 "var_tys G oi r 
   196   \<equiv> case r of 
   197       Heap a \<Rightarrow> (case oi of 
   198                    CInst C \<Rightarrow> fields_table G C (\<lambda>n f. \<not>static f) (+) empty
   199                  | Arr T k \<Rightarrow> empty (+) arr_comps T k)
   200     | Stat C \<Rightarrow> fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) 
   201                 (+) empty"
   202 
   203 lemma var_tys_Some_eq: 
   204  "var_tys G oi r n = Some T 
   205   = (case r of 
   206        Inl a \<Rightarrow> (case oi of  
   207                    CInst C \<Rightarrow> (\<exists>nt. n = Inl nt \<and> fields_table G C (\<lambda>n f. 
   208                                \<not>static f) nt = Some T)  
   209                  | Arr t k \<Rightarrow> (\<exists> i. n = Inr i  \<and> i in_bounds k \<and> t = T))  
   210      | Inr C \<Rightarrow> (\<exists>nt. n = Inl nt \<and> 
   211                  fields_table G C (\<lambda>fn f. declclassf fn = C \<and> static f) nt 
   212                   = Some T))"
   213 apply (unfold var_tys_def arr_comps_def)
   214 apply (force split add: sum.split_asm sum.split obj_tag.split)
   215 done
   216 
   217 
   218 section "stores"
   219 
   220 types	globs                  (* global variables: heap and static variables *)
   221 	= "(oref , obj) table"
   222 	heap
   223 	= "(loc  , obj) table"
   224 	locals
   225 	= "(lname, val) table" (* local variables *)
   226 
   227 translations
   228  "globs"  <= (type) "(oref , obj) table"
   229  "heap"   <= (type) "(loc  , obj) table"
   230  "locals" <= (type) "(lname, val) table"
   231 
   232 datatype st = (* pure state, i.e. contents of all variables *)
   233 	 st globs locals
   234 
   235 subsection "access"
   236 
   237 constdefs
   238 
   239   globs  :: "st \<Rightarrow> globs"
   240  "globs  \<equiv> st_case (\<lambda>g l. g)"
   241   
   242   locals :: "st \<Rightarrow> locals"
   243  "locals \<equiv> st_case (\<lambda>g l. l)"
   244 
   245   heap   :: "st \<Rightarrow> heap"
   246  "heap s \<equiv> globs s \<circ> Heap"
   247 
   248 
   249 lemma globs_def2 [simp]: " globs (st g l) = g"
   250 by (simp add: globs_def)
   251 
   252 lemma locals_def2 [simp]: "locals (st g l) = l"
   253 by (simp add: locals_def)
   254 
   255 lemma heap_def2 [simp]:  "heap s a=globs s (Heap a)"
   256 by (simp add: heap_def)
   257 
   258 
   259 syntax
   260   val_this     :: "st \<Rightarrow> val"
   261   lookup_obj   :: "st \<Rightarrow> val \<Rightarrow> obj"
   262 
   263 translations
   264  "val_this s"       == "the (locals s This)" 
   265  "lookup_obj s a'"  == "the (heap s (the_Addr a'))"
   266 
   267 subsection "memory allocation"
   268 
   269 constdefs
   270   new_Addr     :: "heap \<Rightarrow> loc option"
   271  "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (\<epsilon>a. h a = None)"
   272 
   273 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
   274 apply (unfold new_Addr_def)
   275 apply auto
   276 apply (case_tac "h (SOME a\<Colon>loc. h a = None)")
   277 apply simp
   278 apply (fast intro: someI2)
   279 done
   280 
   281 lemma new_AddrD2: "new_Addr h = Some a \<Longrightarrow> \<forall>b. h b \<noteq> None \<longrightarrow> b \<noteq> a"
   282 apply (drule new_AddrD)
   283 apply auto
   284 done
   285 
   286 lemma new_Addr_SomeI: "h a = None \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None"
   287 apply (unfold new_Addr_def)
   288 apply (frule not_Some_eq [THEN iffD2])
   289 apply auto
   290 apply  (drule not_Some_eq [THEN iffD2])
   291 apply  auto
   292 apply (fast intro!: someI2)
   293 done
   294 
   295 
   296 subsection "initialization"
   297 
   298 syntax
   299 
   300   init_vals     :: "('a, ty) table \<Rightarrow> ('a, val) table"
   301 
   302 translations
   303  "init_vals vs"    == "option_map default_val \<circ> vs"
   304 
   305 lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
   306 apply (unfold arr_comps_def in_bounds_def)
   307 apply (rule ext)
   308 apply auto
   309 done
   310 
   311 lemma init_arr_comps_step [simp]: 
   312 "0 < j \<Longrightarrow> init_vals (arr_comps T  j    ) =  
   313            init_vals (arr_comps T (j - 1))(j - 1\<mapsto>default_val T)"
   314 apply (unfold arr_comps_def in_bounds_def)
   315 apply (rule ext)
   316 apply auto
   317 done
   318 
   319 subsection "update"
   320 
   321 constdefs
   322   gupd       :: "oref  \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st"        ("gupd'(_\<mapsto>_')"[10,10]1000)
   323  "gupd r obj  \<equiv> st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
   324 
   325   lupd       :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"        ("lupd'(_\<mapsto>_')"[10,10]1000)
   326  "lupd vn v   \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
   327 
   328   upd_gobj   :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st" 
   329  "upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
   330 
   331   set_locals  :: "locals \<Rightarrow> st \<Rightarrow> st"
   332  "set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
   333   
   334   init_obj    :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
   335  "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
   336 
   337 syntax
   338   init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
   339 
   340 translations
   341  "init_class_obj G C" == "init_obj G arbitrary (Inr C)"
   342 
   343 lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
   344 apply (unfold gupd_def)
   345 apply (simp (no_asm))
   346 done
   347 
   348 lemma lupd_def2 [simp]: "lupd(vn\<mapsto>v) (st g l) = st g (l(vn\<mapsto>v))"
   349 apply (unfold lupd_def)
   350 apply (simp (no_asm))
   351 done
   352 
   353 lemma globs_gupd [simp]: "globs  (gupd(r\<mapsto>obj) s) = globs s(r\<mapsto>obj)"
   354 apply (induct "s")
   355 by (simp add: gupd_def)
   356 
   357 lemma globs_lupd [simp]: "globs  (lupd(vn\<mapsto>v ) s) = globs  s"
   358 apply (induct "s")
   359 by (simp add: lupd_def)
   360 
   361 lemma locals_gupd [simp]: "locals (gupd(r\<mapsto>obj) s) = locals s"
   362 apply (induct "s")
   363 by (simp add: gupd_def)
   364 
   365 lemma locals_lupd [simp]: "locals (lupd(vn\<mapsto>v ) s) = locals s(vn\<mapsto>v )"
   366 apply (induct "s")
   367 by (simp add: lupd_def)
   368 
   369 lemma globs_upd_gobj_new [rule_format (no_asm), simp]: 
   370   "globs s r = None \<longrightarrow> globs (upd_gobj r n v s) = globs s"
   371 apply (unfold upd_gobj_def)
   372 apply (induct "s")
   373 apply auto
   374 done
   375 
   376 lemma globs_upd_gobj_upd [rule_format (no_asm), simp]: 
   377 "globs s r=Some obj\<longrightarrow> globs (upd_gobj r n v s) = globs s(r\<mapsto>upd_obj n v obj)"
   378 apply (unfold upd_gobj_def)
   379 apply (induct "s")
   380 apply auto
   381 done
   382 
   383 lemma locals_upd_gobj [simp]: "locals (upd_gobj r n v s) = locals s"
   384 apply (induct "s")
   385 by (simp add: upd_gobj_def) 
   386 
   387 
   388 lemma globs_init_obj [simp]: "globs (init_obj G oi r s) t =  
   389   (if t=r then Some \<lparr>tag=oi,values=init_vals (var_tys G oi r)\<rparr> else globs s t)"
   390 apply (unfold init_obj_def)
   391 apply (simp (no_asm))
   392 done
   393 
   394 lemma locals_init_obj [simp]: "locals (init_obj G oi r s) = locals s"
   395 by (simp add: init_obj_def)
   396   
   397 lemma surjective_st [simp]: "st (globs s) (locals s) = s"
   398 apply (induct "s")
   399 by auto
   400 
   401 lemma surjective_st_init_obj: 
   402  "st (globs (init_obj G oi r s)) (locals s) = init_obj G oi r s"
   403 apply (subst locals_init_obj [THEN sym])
   404 apply (rule surjective_st)
   405 done
   406 
   407 lemma heap_heap_upd [simp]: 
   408   "heap (st (g(Inl a\<mapsto>obj)) l) = heap (st g l)(a\<mapsto>obj)"
   409 apply (rule ext)
   410 apply (simp (no_asm))
   411 done
   412 lemma heap_stat_upd [simp]: "heap (st (g(Inr C\<mapsto>obj)) l) = heap (st g l)"
   413 apply (rule ext)
   414 apply (simp (no_asm))
   415 done
   416 lemma heap_local_upd [simp]: "heap (st g (l(vn\<mapsto>v))) = heap (st g l)"
   417 apply (rule ext)
   418 apply (simp (no_asm))
   419 done
   420 
   421 lemma heap_gupd_Heap [simp]: "heap (gupd(Heap a\<mapsto>obj) s) = heap s(a\<mapsto>obj)"
   422 apply (rule ext)
   423 apply (simp (no_asm))
   424 done
   425 lemma heap_gupd_Stat [simp]: "heap (gupd(Stat C\<mapsto>obj) s) = heap s"
   426 apply (rule ext)
   427 apply (simp (no_asm))
   428 done
   429 lemma heap_lupd [simp]: "heap (lupd(vn\<mapsto>v) s) = heap s"
   430 apply (rule ext)
   431 apply (simp (no_asm))
   432 done
   433 
   434 (*
   435 lemma heap_upd_gobj_Heap: "!!a. heap (upd_gobj (Heap a) n v s) = ?X"
   436 apply (rule ext)
   437 apply (simp (no_asm))
   438 apply (case_tac "globs s (Heap a)")
   439 apply  auto
   440 *)
   441 
   442 lemma heap_upd_gobj_Stat [simp]: "heap (upd_gobj (Stat C) n v s) = heap s"
   443 apply (rule ext)
   444 apply (simp (no_asm))
   445 apply (case_tac "globs s (Stat C)")
   446 apply  auto
   447 done
   448 
   449 lemma set_locals_def2 [simp]: "set_locals l (st g l') = st g l"
   450 apply (unfold set_locals_def)
   451 apply (simp (no_asm))
   452 done
   453 
   454 lemma set_locals_id [simp]: "set_locals (locals s) s = s"
   455 apply (unfold set_locals_def)
   456 apply (induct_tac "s")
   457 apply (simp (no_asm))
   458 done
   459 
   460 lemma set_set_locals [simp]: "set_locals l (set_locals l' s) = set_locals l s"
   461 apply (unfold set_locals_def)
   462 apply (induct_tac "s")
   463 apply (simp (no_asm))
   464 done
   465 
   466 lemma locals_set_locals [simp]: "locals (set_locals l s) = l"
   467 apply (unfold set_locals_def)
   468 apply (induct_tac "s")
   469 apply (simp (no_asm))
   470 done
   471 
   472 lemma globs_set_locals [simp]: "globs (set_locals l s) = globs s"
   473 apply (unfold set_locals_def)
   474 apply (induct_tac "s")
   475 apply (simp (no_asm))
   476 done
   477 
   478 lemma heap_set_locals [simp]: "heap (set_locals l s) = heap s"
   479 apply (unfold heap_def)
   480 apply (induct_tac "s")
   481 apply (simp (no_asm))
   482 done
   483 
   484 
   485 section "abrupt completion"
   486 
   487 
   488 datatype xcpt        (* exception *)
   489 	= Loc loc    (* location of allocated execption object *)
   490 	| Std xname  (* intermediate standard exception, see Eval.thy *)
   491 
   492 datatype abrupt      (* abrupt completion *) 
   493         = Xcpt xcpt  (* exception *)
   494         | Jump jump  (* break, continue, return *)
   495 consts
   496 
   497   the_Xcpt :: "abrupt \<Rightarrow> xcpt"
   498   the_Jump :: "abrupt => jump"
   499   the_Loc  :: "xcpt \<Rightarrow> loc"
   500   the_Std  :: "xcpt \<Rightarrow> xname"
   501 
   502 primrec "the_Xcpt (Xcpt x) = x"
   503 primrec "the_Jump (Jump j) = j"
   504 primrec "the_Loc (Loc a) = a"
   505 primrec "the_Std (Std x) = x"
   506 
   507 types
   508   abopt  = "abrupt option"
   509 	
   510 
   511 constdefs
   512   abrupt_if    :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt"
   513  "abrupt_if c x' x \<equiv> if c \<and> (x = None) then x' else x"
   514 
   515 lemma abrupt_if_True_None [simp]: "abrupt_if True x None = x"
   516 by (simp add: abrupt_if_def)
   517 
   518 lemma abrupt_if_True_not_None [simp]: "x \<noteq> None \<Longrightarrow> abrupt_if True x y \<noteq> None"
   519 by (simp add: abrupt_if_def)
   520 
   521 lemma abrupt_if_False [simp]: "abrupt_if False x y = y"
   522 by (simp add: abrupt_if_def)
   523 
   524 lemma abrupt_if_Some [simp]: "abrupt_if c x (Some y) = Some y"
   525 by (simp add: abrupt_if_def)
   526 
   527 lemma abrupt_if_not_None [simp]: "y \<noteq> None \<Longrightarrow> abrupt_if c x y = y"
   528 apply (simp add: abrupt_if_def)
   529 by auto
   530 
   531 
   532 lemma split_abrupt_if: 
   533 "P (abrupt_if c x' x) = 
   534       ((c \<and> x = None \<longrightarrow> P x') \<and> (\<not> (c \<and> x = None) \<longrightarrow> P x))"
   535 apply (unfold abrupt_if_def)
   536 apply (split split_if)
   537 apply auto
   538 done
   539 
   540 syntax
   541 
   542   raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
   543   np       :: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
   544   check_neg:: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
   545   
   546 translations
   547 
   548  "raise_if c xn" == "abrupt_if c (Some (Xcpt (Std xn)))"
   549  "np v"          == "raise_if (v = Null)      NullPointer"
   550  "check_neg i'"  == "raise_if (the_Intg i'<0) NegArrSize"
   551 
   552 lemma raise_if_None [simp]: "(raise_if c x y = None) = (\<not>c \<and> y = None)"
   553 apply (simp add: abrupt_if_def)
   554 by auto
   555 declare raise_if_None [THEN iffD1, dest!]
   556 
   557 lemma if_raise_if_None [simp]: 
   558   "((if b then y else raise_if c x y) = None) = ((c \<longrightarrow> b) \<and> y = None)"
   559 apply (simp add: abrupt_if_def)
   560 apply auto
   561 done
   562 
   563 lemma raise_if_SomeD [dest!]:
   564   "raise_if c x y = Some z \<Longrightarrow> c \<and> z=(Xcpt (Std x)) \<and> y=None \<or> (y=Some z)"
   565 apply (case_tac y)
   566 apply (case_tac c)
   567 apply (simp add: abrupt_if_def)
   568 apply (simp add: abrupt_if_def)
   569 apply auto
   570 done
   571 
   572 constdefs
   573    absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt"
   574   "absorb j a \<equiv> if a=Some (Jump j) then None else a"
   575 
   576 lemma absorb_SomeD [dest!]: "absorb j a = Some x \<Longrightarrow> a = Some x"
   577 by (auto simp add: absorb_def)
   578 
   579 lemma absorb_same [simp]: "absorb j (Some (Jump j)) = None"
   580 by (auto simp add: absorb_def)
   581 
   582 lemma absorb_other [simp]: "a \<noteq> Some (Jump j) \<Longrightarrow> absorb j a = a"
   583 by (auto simp add: absorb_def)
   584 
   585 
   586 section "full program state"
   587 
   588 types
   589   state = "abopt \<times> st"          (* state including exception information *)
   590 
   591 syntax 
   592   Norm   :: "st \<Rightarrow> state"
   593   abrupt :: "state \<Rightarrow> abopt"
   594   store  :: "state \<Rightarrow> st"
   595 
   596 translations
   597    
   598   "Norm s"     == "(None,s)" 
   599   "abrupt"     => "fst"
   600   "store"      => "snd"
   601   "abopt"       <= (type) "State.abrupt option"
   602   "abopt"       <= (type) "abrupt option"
   603   "state"      <= (type) "abopt \<times> State.st"
   604   "state"      <= (type) "abopt \<times> st"
   605 
   606 
   607 
   608 lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False"
   609 apply (erule_tac x = "(Some k,y)" in all_dupE)
   610 apply (erule_tac x = "(None,y)" in allE)
   611 apply clarify
   612 done
   613 
   614 lemma state_not_single: "All (op = (x::state)) \<Longrightarrow> R"
   615 apply (drule_tac x = "(if abrupt x = None then Some ?x else None,?y)" in spec)
   616 apply clarsimp
   617 done
   618 
   619 constdefs
   620 
   621   normal     :: "state \<Rightarrow> bool"
   622  "normal \<equiv> \<lambda>s. abrupt s = None"
   623 
   624 lemma normal_def2 [simp]: "normal s = (abrupt s = None)"
   625 apply (unfold normal_def)
   626 apply (simp (no_asm))
   627 done
   628 
   629 constdefs
   630   heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool"
   631  "heap_free n \<equiv> \<lambda>s. atleast_free (heap (store s)) n"
   632 
   633 lemma heap_free_def2 [simp]: "heap_free n s = atleast_free (heap (store s)) n"
   634 apply (unfold heap_free_def)
   635 apply simp
   636 done
   637 
   638 subsection "update"
   639 
   640 constdefs
   641  
   642   abupd     :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
   643  "abupd f \<equiv> prod_fun f id"
   644 
   645   supd     :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state" 
   646  "supd \<equiv> prod_fun id"
   647   
   648 lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
   649 by (simp add: abupd_def)
   650 
   651 lemma abupd_abrupt_if_False [simp]: "\<And> s. abupd (abrupt_if False xo) s = s"
   652 by simp
   653 
   654 lemma supd_def2 [simp]: "supd f (x,s) = (x,f s)"
   655 by (simp add: supd_def)
   656 
   657 lemma supd_lupd [simp]: 
   658  "\<And> s. supd (lupd vn v ) s = (abrupt s,lupd vn v (store s))"
   659 apply (simp (no_asm_simp) only: split_tupled_all)
   660 apply (simp (no_asm))
   661 done
   662 
   663 
   664 lemma supd_gupd [simp]: 
   665  "\<And> s. supd (gupd r obj) s = (abrupt s,gupd r obj (store s))"
   666 apply (simp (no_asm_simp) only: split_tupled_all)
   667 apply (simp (no_asm))
   668 done
   669 
   670 lemma supd_init_obj [simp]: 
   671  "supd (init_obj G oi r) s = (abrupt s,init_obj G oi r (store s))"
   672 apply (unfold init_obj_def)
   673 apply (simp (no_asm))
   674 done
   675 
   676 syntax
   677 
   678   set_lvars     :: "locals \<Rightarrow> state \<Rightarrow> state"
   679   restore_lvars :: "state  \<Rightarrow> state \<Rightarrow> state"
   680   
   681 translations
   682 
   683  "set_lvars l" == "supd (set_locals l)"
   684  "restore_lvars s' s" == "set_lvars (locals (store s')) s"
   685 
   686 lemma set_set_lvars [simp]: "\<And> s. set_lvars l (set_lvars l' s) = set_lvars l s"
   687 apply (simp (no_asm_simp) only: split_tupled_all)
   688 apply (simp (no_asm))
   689 done
   690 
   691 lemma set_lvars_id [simp]: "\<And> s. set_lvars (locals (store s)) s = s"
   692 apply (simp (no_asm_simp) only: split_tupled_all)
   693 apply (simp (no_asm))
   694 done
   695 
   696 section "initialisation test"
   697 
   698 constdefs
   699 
   700   inited   :: "qtname \<Rightarrow> globs \<Rightarrow> bool"
   701  "inited C g \<equiv> g (Stat C) \<noteq> None"
   702 
   703   initd    :: "qtname \<Rightarrow> state \<Rightarrow> bool"
   704  "initd C \<equiv> inited C \<circ> globs \<circ> store"
   705 
   706 lemma not_inited_empty [simp]: "\<not>inited C empty"
   707 apply (unfold inited_def)
   708 apply (simp (no_asm))
   709 done
   710 
   711 lemma inited_gupdate [simp]: "inited C (g(r\<mapsto>obj)) = (inited C g \<or> r = Stat C)"
   712 apply (unfold inited_def)
   713 apply (auto split add: st.split)
   714 done
   715 
   716 lemma inited_init_class_obj [intro!]: "inited C (globs (init_class_obj G C s))"
   717 apply (unfold inited_def)
   718 apply (simp (no_asm))
   719 done
   720 
   721 lemma not_initedD: "\<not> inited C g \<Longrightarrow> g (Stat C) = None"
   722 apply (unfold inited_def)
   723 apply (erule notnotD)
   724 done
   725 
   726 lemma initedD: "inited C g \<Longrightarrow> \<exists> obj. g (Stat C) = Some obj"
   727 apply (unfold inited_def)
   728 apply auto
   729 done
   730 
   731 lemma initd_def2 [simp]: "initd C s = inited C (globs (store s))"
   732 apply (unfold initd_def)
   733 apply (simp (no_asm))
   734 done
   735 
   736 
   737 
   738 end
   739