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