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