src/HOL/Bali/State.thy
author skalberg
Thu Aug 28 01:56:40 2003 +0200 (2003-08-28)
changeset 14171 0cab06e3bbd0
parent 13688 a0b16d42d489
child 14766 c0401da7726d
permissions -rw-r--r--
Extended the notion of letter and digit, such that now one may use greek,
gothic, euler, or calligraphic letters as normal letters.
     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