src/HOL/Bali/State.thy
author haftmann
Fri Nov 27 08:42:50 2009 +0100 (2009-11-27)
changeset 33965 f57c11db4ad4
parent 32960 69916a850301
child 35067 af4c18c30593
permissions -rw-r--r--
Inl and Inr now with authentic syntax
     1 (*  Title:      HOL/Bali/State.thy
     2     Author:     David von Oheimb
     3 *)
     4 header {* State for evaluation of Java expressions and statements *}
     5 
     6 theory State
     7 imports DeclConcepts
     8 begin
     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> SOME (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" => "CONST Inl"
   143   "Stat" => "CONST 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"       == "CONST the (locals s This)" 
   263  "lookup_obj s a'"  == "CONST 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 (SOME a. h a = None)"
   270 
   271 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
   272 apply (auto simp add: new_Addr_def)
   273 apply (erule someI) 
   274 done
   275 
   276 lemma new_AddrD2: "new_Addr h = Some a \<Longrightarrow> \<forall>b. h b \<noteq> None \<longrightarrow> b \<noteq> a"
   277 apply (drule new_AddrD)
   278 apply auto
   279 done
   280 
   281 lemma new_Addr_SomeI: "h a = None \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None"
   282 apply (simp add: new_Addr_def)
   283 apply (fast intro: someI2)
   284 done
   285 
   286 
   287 subsection "initialization"
   288 
   289 syntax
   290 
   291   init_vals     :: "('a, ty) table \<Rightarrow> ('a, val) table"
   292 
   293 translations
   294  "init_vals vs"    == "CONST Option.map default_val \<circ> vs"
   295 
   296 lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
   297 apply (unfold arr_comps_def in_bounds_def)
   298 apply (rule ext)
   299 apply auto
   300 done
   301 
   302 lemma init_arr_comps_step [simp]: 
   303 "0 < j \<Longrightarrow> init_vals (arr_comps T  j    ) =  
   304            init_vals (arr_comps T (j - 1))(j - 1\<mapsto>default_val T)"
   305 apply (unfold arr_comps_def in_bounds_def)
   306 apply (rule ext)
   307 apply auto
   308 done
   309 
   310 subsection "update"
   311 
   312 constdefs
   313   gupd       :: "oref  \<Rightarrow> obj \<Rightarrow> st \<Rightarrow> st"        ("gupd'(_\<mapsto>_')"[10,10]1000)
   314  "gupd r obj  \<equiv> st_case (\<lambda>g l. st (g(r\<mapsto>obj)) l)"
   315 
   316   lupd       :: "lname \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"        ("lupd'(_\<mapsto>_')"[10,10]1000)
   317  "lupd vn v   \<equiv> st_case (\<lambda>g l. st g (l(vn\<mapsto>v)))"
   318 
   319   upd_gobj   :: "oref \<Rightarrow> vn \<Rightarrow> val \<Rightarrow> st \<Rightarrow> st"
   320  "upd_gobj r n v \<equiv> st_case (\<lambda>g l. st (chg_map (upd_obj n v) r g) l)"
   321 
   322   set_locals  :: "locals \<Rightarrow> st \<Rightarrow> st"
   323  "set_locals l \<equiv> st_case (\<lambda>g l'. st g l)"
   324 
   325   init_obj    :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
   326  "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
   327 
   328 syntax
   329   init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
   330 
   331 translations
   332  "init_class_obj G C" == "init_obj G CONST undefined (CONST Inr C)"
   333 
   334 lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
   335 apply (unfold gupd_def)
   336 apply (simp (no_asm))
   337 done
   338 
   339 lemma lupd_def2 [simp]: "lupd(vn\<mapsto>v) (st g l) = st g (l(vn\<mapsto>v))"
   340 apply (unfold lupd_def)
   341 apply (simp (no_asm))
   342 done
   343 
   344 lemma globs_gupd [simp]: "globs  (gupd(r\<mapsto>obj) s) = globs s(r\<mapsto>obj)"
   345 apply (induct "s")
   346 by (simp add: gupd_def)
   347 
   348 lemma globs_lupd [simp]: "globs  (lupd(vn\<mapsto>v ) s) = globs  s"
   349 apply (induct "s")
   350 by (simp add: lupd_def)
   351 
   352 lemma locals_gupd [simp]: "locals (gupd(r\<mapsto>obj) s) = locals s"
   353 apply (induct "s")
   354 by (simp add: gupd_def)
   355 
   356 lemma locals_lupd [simp]: "locals (lupd(vn\<mapsto>v ) s) = locals s(vn\<mapsto>v )"
   357 apply (induct "s")
   358 by (simp add: lupd_def)
   359 
   360 lemma globs_upd_gobj_new [rule_format (no_asm), simp]: 
   361   "globs s r = None \<longrightarrow> globs (upd_gobj r n v s) = globs s"
   362 apply (unfold upd_gobj_def)
   363 apply (induct "s")
   364 apply auto
   365 done
   366 
   367 lemma globs_upd_gobj_upd [rule_format (no_asm), simp]: 
   368 "globs s r=Some obj\<longrightarrow> globs (upd_gobj r n v s) = globs s(r\<mapsto>upd_obj n v obj)"
   369 apply (unfold upd_gobj_def)
   370 apply (induct "s")
   371 apply auto
   372 done
   373 
   374 lemma locals_upd_gobj [simp]: "locals (upd_gobj r n v s) = locals s"
   375 apply (induct "s")
   376 by (simp add: upd_gobj_def) 
   377 
   378 
   379 lemma globs_init_obj [simp]: "globs (init_obj G oi r s) t =  
   380   (if t=r then Some \<lparr>tag=oi,values=init_vals (var_tys G oi r)\<rparr> else globs s t)"
   381 apply (unfold init_obj_def)
   382 apply (simp (no_asm))
   383 done
   384 
   385 lemma locals_init_obj [simp]: "locals (init_obj G oi r s) = locals s"
   386 by (simp add: init_obj_def)
   387   
   388 lemma surjective_st [simp]: "st (globs s) (locals s) = s"
   389 apply (induct "s")
   390 by auto
   391 
   392 lemma surjective_st_init_obj: 
   393  "st (globs (init_obj G oi r s)) (locals s) = init_obj G oi r s"
   394 apply (subst locals_init_obj [THEN sym])
   395 apply (rule surjective_st)
   396 done
   397 
   398 lemma heap_heap_upd [simp]: 
   399   "heap (st (g(Inl a\<mapsto>obj)) l) = heap (st g l)(a\<mapsto>obj)"
   400 apply (rule ext)
   401 apply (simp (no_asm))
   402 done
   403 lemma heap_stat_upd [simp]: "heap (st (g(Inr C\<mapsto>obj)) l) = heap (st g l)"
   404 apply (rule ext)
   405 apply (simp (no_asm))
   406 done
   407 lemma heap_local_upd [simp]: "heap (st g (l(vn\<mapsto>v))) = heap (st g l)"
   408 apply (rule ext)
   409 apply (simp (no_asm))
   410 done
   411 
   412 lemma heap_gupd_Heap [simp]: "heap (gupd(Heap a\<mapsto>obj) s) = heap s(a\<mapsto>obj)"
   413 apply (rule ext)
   414 apply (simp (no_asm))
   415 done
   416 lemma heap_gupd_Stat [simp]: "heap (gupd(Stat C\<mapsto>obj) s) = heap s"
   417 apply (rule ext)
   418 apply (simp (no_asm))
   419 done
   420 lemma heap_lupd [simp]: "heap (lupd(vn\<mapsto>v) s) = heap s"
   421 apply (rule ext)
   422 apply (simp (no_asm))
   423 done
   424 
   425 lemma heap_upd_gobj_Stat [simp]: "heap (upd_gobj (Stat C) n v s) = heap s"
   426 apply (rule ext)
   427 apply (simp (no_asm))
   428 apply (case_tac "globs s (Stat C)")
   429 apply  auto
   430 done
   431 
   432 lemma set_locals_def2 [simp]: "set_locals l (st g l') = st g l"
   433 apply (unfold set_locals_def)
   434 apply (simp (no_asm))
   435 done
   436 
   437 lemma set_locals_id [simp]: "set_locals (locals s) s = s"
   438 apply (unfold set_locals_def)
   439 apply (induct_tac "s")
   440 apply (simp (no_asm))
   441 done
   442 
   443 lemma set_set_locals [simp]: "set_locals l (set_locals l' s) = set_locals l s"
   444 apply (unfold set_locals_def)
   445 apply (induct_tac "s")
   446 apply (simp (no_asm))
   447 done
   448 
   449 lemma locals_set_locals [simp]: "locals (set_locals l s) = l"
   450 apply (unfold set_locals_def)
   451 apply (induct_tac "s")
   452 apply (simp (no_asm))
   453 done
   454 
   455 lemma globs_set_locals [simp]: "globs (set_locals l s) = globs s"
   456 apply (unfold set_locals_def)
   457 apply (induct_tac "s")
   458 apply (simp (no_asm))
   459 done
   460 
   461 lemma heap_set_locals [simp]: "heap (set_locals l s) = heap s"
   462 apply (unfold heap_def)
   463 apply (induct_tac "s")
   464 apply (simp (no_asm))
   465 done
   466 
   467 
   468 section "abrupt completion"
   469 
   470 
   471 
   472 consts
   473 
   474   the_Xcpt :: "abrupt \<Rightarrow> xcpt"
   475   the_Jump :: "abrupt => jump"
   476   the_Loc  :: "xcpt \<Rightarrow> loc"
   477   the_Std  :: "xcpt \<Rightarrow> xname"
   478 
   479 primrec "the_Xcpt (Xcpt x) = x"
   480 primrec "the_Jump (Jump j) = j"
   481 primrec "the_Loc (Loc a) = a"
   482 primrec "the_Std (Std x) = x"
   483 
   484 
   485         
   486 
   487 constdefs
   488   abrupt_if    :: "bool \<Rightarrow> abopt \<Rightarrow> abopt \<Rightarrow> abopt"
   489  "abrupt_if c x' x \<equiv> if c \<and> (x = None) then x' else x"
   490 
   491 lemma abrupt_if_True_None [simp]: "abrupt_if True x None = x"
   492 by (simp add: abrupt_if_def)
   493 
   494 lemma abrupt_if_True_not_None [simp]: "x \<noteq> None \<Longrightarrow> abrupt_if True x y \<noteq> None"
   495 by (simp add: abrupt_if_def)
   496 
   497 lemma abrupt_if_False [simp]: "abrupt_if False x y = y"
   498 by (simp add: abrupt_if_def)
   499 
   500 lemma abrupt_if_Some [simp]: "abrupt_if c x (Some y) = Some y"
   501 by (simp add: abrupt_if_def)
   502 
   503 lemma abrupt_if_not_None [simp]: "y \<noteq> None \<Longrightarrow> abrupt_if c x y = y"
   504 apply (simp add: abrupt_if_def)
   505 by auto
   506 
   507 
   508 lemma split_abrupt_if: 
   509 "P (abrupt_if c x' x) = 
   510       ((c \<and> x = None \<longrightarrow> P x') \<and> (\<not> (c \<and> x = None) \<longrightarrow> P x))"
   511 apply (unfold abrupt_if_def)
   512 apply (split split_if)
   513 apply auto
   514 done
   515 
   516 syntax
   517 
   518   raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
   519   np       :: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
   520   check_neg:: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
   521   error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt"
   522   
   523 translations
   524 
   525  "raise_if c xn" == "abrupt_if c (Some (Xcpt (Std xn)))"
   526  "np v"          == "raise_if (v = Null)      NullPointer"
   527  "check_neg i'"  == "raise_if (the_Intg i'<0) NegArrSize"
   528  "error_if c e"  == "abrupt_if c (Some (Error e))"
   529 
   530 lemma raise_if_None [simp]: "(raise_if c x y = None) = (\<not>c \<and> y = None)"
   531 apply (simp add: abrupt_if_def)
   532 by auto
   533 declare raise_if_None [THEN iffD1, dest!]
   534 
   535 lemma if_raise_if_None [simp]: 
   536   "((if b then y else raise_if c x y) = None) = ((c \<longrightarrow> b) \<and> y = None)"
   537 apply (simp add: abrupt_if_def)
   538 apply auto
   539 done
   540 
   541 lemma raise_if_SomeD [dest!]:
   542   "raise_if c x y = Some z \<Longrightarrow> c \<and> z=(Xcpt (Std x)) \<and> y=None \<or> (y=Some z)"
   543 apply (case_tac y)
   544 apply (case_tac c)
   545 apply (simp add: abrupt_if_def)
   546 apply (simp add: abrupt_if_def)
   547 apply auto
   548 done
   549 
   550 lemma error_if_None [simp]: "(error_if c e y = None) = (\<not>c \<and> y = None)"
   551 apply (simp add: abrupt_if_def)
   552 by auto
   553 declare error_if_None [THEN iffD1, dest!]
   554 
   555 lemma if_error_if_None [simp]: 
   556   "((if b then y else error_if c e y) = None) = ((c \<longrightarrow> b) \<and> y = None)"
   557 apply (simp add: abrupt_if_def)
   558 apply auto
   559 done
   560 
   561 lemma error_if_SomeD [dest!]:
   562   "error_if c e y = Some z \<Longrightarrow> c \<and> z=(Error e) \<and> y=None \<or> (y=Some z)"
   563 apply (case_tac y)
   564 apply (case_tac c)
   565 apply (simp add: abrupt_if_def)
   566 apply (simp add: abrupt_if_def)
   567 apply auto
   568 done
   569 
   570 constdefs
   571    absorb :: "jump \<Rightarrow> abopt \<Rightarrow> abopt"
   572   "absorb j a \<equiv> if a=Some (Jump j) then None else a"
   573 
   574 lemma absorb_SomeD [dest!]: "absorb j a = Some x \<Longrightarrow> a = Some x"
   575 by (auto simp add: absorb_def)
   576 
   577 lemma absorb_same [simp]: "absorb j (Some (Jump j)) = None"
   578 by (auto simp add: absorb_def)
   579 
   580 lemma absorb_other [simp]: "a \<noteq> Some (Jump j) \<Longrightarrow> absorb j a = a"
   581 by (auto simp add: absorb_def)
   582 
   583 lemma absorb_Some_NoneD: "absorb j (Some abr) = None \<Longrightarrow> abr = Jump j"
   584   by (simp add: absorb_def)
   585 
   586 lemma absorb_Some_JumpD: "absorb j s = Some (Jump j') \<Longrightarrow> j'\<noteq>j"
   587   by (simp add: absorb_def)
   588 
   589 
   590 section "full program state"
   591 
   592 types
   593   state = "abopt \<times> st"          --{* state including abruption information *}
   594 
   595 syntax 
   596   Norm   :: "st \<Rightarrow> state"
   597   abrupt :: "state \<Rightarrow> abopt"
   598   store  :: "state \<Rightarrow> st"
   599 
   600 translations
   601    
   602   "Norm s"     == "(None,s)" 
   603   "abrupt"     => "fst"
   604   "store"      => "snd"
   605   "abopt"       <= (type) "State.abrupt option"
   606   "abopt"       <= (type) "abrupt option"
   607   "state"      <= (type) "abopt \<times> State.st"
   608   "state"      <= (type) "abopt \<times> st"
   609 
   610 
   611 
   612 lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False"
   613 apply (erule_tac x = "(Some k,y)" in all_dupE)
   614 apply (erule_tac x = "(None,y)" in allE)
   615 apply clarify
   616 done
   617 
   618 lemma state_not_single: "All (op = (x::state)) \<Longrightarrow> R"
   619 apply (drule_tac x = "(if abrupt x = None then Some ?x else None,?y)" in spec)
   620 apply clarsimp
   621 done
   622 
   623 constdefs
   624 
   625   normal     :: "state \<Rightarrow> bool"
   626  "normal \<equiv> \<lambda>s. abrupt s = None"
   627 
   628 lemma normal_def2 [simp]: "normal s = (abrupt s = None)"
   629 apply (unfold normal_def)
   630 apply (simp (no_asm))
   631 done
   632 
   633 constdefs
   634   heap_free :: "nat \<Rightarrow> state \<Rightarrow> bool"
   635  "heap_free n \<equiv> \<lambda>s. atleast_free (heap (store s)) n"
   636 
   637 lemma heap_free_def2 [simp]: "heap_free n s = atleast_free (heap (store s)) n"
   638 apply (unfold heap_free_def)
   639 apply simp
   640 done
   641 
   642 subsection "update"
   643 
   644 constdefs
   645  
   646   abupd     :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
   647  "abupd f \<equiv> prod_fun f id"
   648 
   649   supd     :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state" 
   650  "supd \<equiv> prod_fun id"
   651   
   652 lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
   653 by (simp add: abupd_def)
   654 
   655 lemma abupd_abrupt_if_False [simp]: "\<And> s. abupd (abrupt_if False xo) s = s"
   656 by simp
   657 
   658 lemma supd_def2 [simp]: "supd f (x,s) = (x,f s)"
   659 by (simp add: supd_def)
   660 
   661 lemma supd_lupd [simp]: 
   662  "\<And> s. supd (lupd vn v ) s = (abrupt s,lupd vn v (store s))"
   663 apply (simp (no_asm_simp) only: split_tupled_all)
   664 apply (simp (no_asm))
   665 done
   666 
   667 
   668 lemma supd_gupd [simp]: 
   669  "\<And> s. supd (gupd r obj) s = (abrupt s,gupd r obj (store s))"
   670 apply (simp (no_asm_simp) only: split_tupled_all)
   671 apply (simp (no_asm))
   672 done
   673 
   674 lemma supd_init_obj [simp]: 
   675  "supd (init_obj G oi r) s = (abrupt s,init_obj G oi r (store s))"
   676 apply (unfold init_obj_def)
   677 apply (simp (no_asm))
   678 done
   679 
   680 lemma abupd_store_invariant [simp]: "store (abupd f s) = store s"
   681   by (cases s) simp
   682 
   683 lemma supd_abrupt_invariant [simp]: "abrupt (supd f s) = abrupt s"
   684   by (cases s) simp
   685 
   686 syntax
   687 
   688   set_lvars     :: "locals \<Rightarrow> state \<Rightarrow> state"
   689   restore_lvars :: "state  \<Rightarrow> state \<Rightarrow> state"
   690   
   691 translations
   692 
   693  "set_lvars l" == "supd (set_locals l)"
   694  "restore_lvars s' s" == "set_lvars (locals (store s')) s"
   695 
   696 lemma set_set_lvars [simp]: "\<And> s. set_lvars l (set_lvars l' s) = set_lvars l s"
   697 apply (simp (no_asm_simp) only: split_tupled_all)
   698 apply (simp (no_asm))
   699 done
   700 
   701 lemma set_lvars_id [simp]: "\<And> s. set_lvars (locals (store s)) s = s"
   702 apply (simp (no_asm_simp) only: split_tupled_all)
   703 apply (simp (no_asm))
   704 done
   705 
   706 section "initialisation test"
   707 
   708 constdefs
   709 
   710   inited   :: "qtname \<Rightarrow> globs \<Rightarrow> bool"
   711  "inited C g \<equiv> g (Stat C) \<noteq> None"
   712 
   713   initd    :: "qtname \<Rightarrow> state \<Rightarrow> bool"
   714  "initd C \<equiv> inited C \<circ> globs \<circ> store"
   715 
   716 lemma not_inited_empty [simp]: "\<not>inited C empty"
   717 apply (unfold inited_def)
   718 apply (simp (no_asm))
   719 done
   720 
   721 lemma inited_gupdate [simp]: "inited C (g(r\<mapsto>obj)) = (inited C g \<or> r = Stat C)"
   722 apply (unfold inited_def)
   723 apply (auto split add: st.split)
   724 done
   725 
   726 lemma inited_init_class_obj [intro!]: "inited C (globs (init_class_obj G C s))"
   727 apply (unfold inited_def)
   728 apply (simp (no_asm))
   729 done
   730 
   731 lemma not_initedD: "\<not> inited C g \<Longrightarrow> g (Stat C) = None"
   732 apply (unfold inited_def)
   733 apply (erule notnotD)
   734 done
   735 
   736 lemma initedD: "inited C g \<Longrightarrow> \<exists> obj. g (Stat C) = Some obj"
   737 apply (unfold inited_def)
   738 apply auto
   739 done
   740 
   741 lemma initd_def2 [simp]: "initd C s = inited C (globs (store s))"
   742 apply (unfold initd_def)
   743 apply (simp (no_asm))
   744 done
   745 
   746 section {* @{text error_free} *}
   747 constdefs error_free:: "state \<Rightarrow> bool"
   748 "error_free s \<equiv> \<not> (\<exists> err. abrupt s = Some (Error err))"
   749 
   750 lemma error_free_Norm [simp,intro]: "error_free (Norm s)"
   751 by (simp add: error_free_def)
   752 
   753 lemma error_free_normal [simp,intro]: "normal s \<Longrightarrow> error_free s"
   754 by (simp add: error_free_def)
   755 
   756 lemma error_free_Xcpt [simp]: "error_free (Some (Xcpt x),s)"
   757 by (simp add: error_free_def)
   758 
   759 lemma error_free_Jump [simp,intro]: "error_free (Some (Jump j),s)"
   760 by (simp add: error_free_def)
   761 
   762 lemma error_free_Error [simp]: "error_free (Some (Error e),s) = False"
   763 by (simp add: error_free_def)  
   764 
   765 lemma error_free_Some [simp,intro]: 
   766  "\<not> (\<exists> err. x=Error err) \<Longrightarrow> error_free ((Some x),s)"
   767 by (auto simp add: error_free_def)
   768 
   769 lemma error_free_abupd_absorb [simp,intro]: 
   770  "error_free s \<Longrightarrow> error_free (abupd (absorb j) s)"
   771 by (cases s) 
   772    (auto simp add: error_free_def absorb_def
   773          split: split_if_asm)
   774 
   775 lemma error_free_absorb [simp,intro]: 
   776  "error_free (a,s) \<Longrightarrow> error_free (absorb j a, s)"
   777 by (auto simp add: error_free_def absorb_def
   778             split: split_if_asm)
   779 
   780 lemma error_free_abrupt_if [simp,intro]:
   781 "\<lbrakk>error_free s; \<not> (\<exists> err. x=Error err)\<rbrakk>
   782  \<Longrightarrow> error_free (abupd (abrupt_if p (Some x)) s)"
   783 by (cases s)
   784    (auto simp add: abrupt_if_def
   785             split: split_if)
   786 
   787 lemma error_free_abrupt_if1 [simp,intro]:
   788 "\<lbrakk>error_free (a,s); \<not> (\<exists> err. x=Error err)\<rbrakk>
   789  \<Longrightarrow> error_free (abrupt_if p (Some x) a, s)"
   790 by  (auto simp add: abrupt_if_def
   791             split: split_if)
   792 
   793 lemma error_free_abrupt_if_Xcpt [simp,intro]:
   794  "error_free s 
   795   \<Longrightarrow> error_free (abupd (abrupt_if p (Some (Xcpt x))) s)"
   796 by simp 
   797 
   798 lemma error_free_abrupt_if_Xcpt1 [simp,intro]:
   799  "error_free (a,s) 
   800   \<Longrightarrow> error_free (abrupt_if p (Some (Xcpt x)) a, s)" 
   801 by simp 
   802 
   803 lemma error_free_abrupt_if_Jump [simp,intro]:
   804  "error_free s 
   805   \<Longrightarrow> error_free (abupd (abrupt_if p (Some (Jump j))) s)" 
   806 by simp
   807 
   808 lemma error_free_abrupt_if_Jump1 [simp,intro]:
   809  "error_free (a,s) 
   810   \<Longrightarrow> error_free (abrupt_if p (Some (Jump j)) a, s)" 
   811 by simp
   812 
   813 lemma error_free_raise_if [simp,intro]:
   814  "error_free s \<Longrightarrow> error_free (abupd (raise_if p x) s)"
   815 by simp 
   816 
   817 lemma error_free_raise_if1 [simp,intro]:
   818  "error_free (a,s) \<Longrightarrow> error_free ((raise_if p x a), s)"
   819 by simp 
   820 
   821 lemma error_free_supd [simp,intro]:
   822  "error_free s \<Longrightarrow> error_free (supd f s)"
   823 by (cases s) (simp add: error_free_def)
   824 
   825 lemma error_free_supd1 [simp,intro]:
   826  "error_free (a,s) \<Longrightarrow> error_free (a,f s)"
   827 by (simp add: error_free_def)
   828 
   829 lemma error_free_set_lvars [simp,intro]:
   830 "error_free s \<Longrightarrow> error_free ((set_lvars l) s)"
   831 by (cases s) simp
   832 
   833 lemma error_free_set_locals [simp,intro]: 
   834 "error_free (x, s)
   835        \<Longrightarrow> error_free (x, set_locals l s')"
   836 by (simp add: error_free_def)
   837 
   838 
   839 end
   840