src/HOL/Bali/State.thy
changeset 35067 af4c18c30593
parent 33965 f57c11db4ad4
child 35416 d8d7d1b785af
     1.1 --- a/src/HOL/Bali/State.thy	Tue Feb 09 16:07:09 2010 +0100
     1.2 +++ b/src/HOL/Bali/State.thy	Wed Feb 10 00:45:16 2010 +0100
     1.3 @@ -254,13 +254,11 @@
     1.4  by (simp add: heap_def)
     1.5  
     1.6  
     1.7 -syntax
     1.8 -  val_this     :: "st \<Rightarrow> val"
     1.9 -  lookup_obj   :: "st \<Rightarrow> val \<Rightarrow> obj"
    1.10 +abbreviation val_this :: "st \<Rightarrow> val"
    1.11 +  where "val_this s == the (locals s This)"
    1.12  
    1.13 -translations
    1.14 - "val_this s"       == "CONST the (locals s This)" 
    1.15 - "lookup_obj s a'"  == "CONST the (heap s (the_Addr a'))"
    1.16 +abbreviation lookup_obj :: "st \<Rightarrow> val \<Rightarrow> obj"
    1.17 +  where "lookup_obj s a' == the (heap s (the_Addr a'))"
    1.18  
    1.19  subsection "memory allocation"
    1.20  
    1.21 @@ -286,12 +284,8 @@
    1.22  
    1.23  subsection "initialization"
    1.24  
    1.25 -syntax
    1.26 -
    1.27 -  init_vals     :: "('a, ty) table \<Rightarrow> ('a, val) table"
    1.28 -
    1.29 -translations
    1.30 - "init_vals vs"    == "CONST Option.map default_val \<circ> vs"
    1.31 +abbreviation init_vals :: "('a, ty) table \<Rightarrow> ('a, val) table"
    1.32 +  where "init_vals vs == Option.map default_val \<circ> vs"
    1.33  
    1.34  lemma init_arr_comps_base [simp]: "init_vals (arr_comps T 0) = empty"
    1.35  apply (unfold arr_comps_def in_bounds_def)
    1.36 @@ -325,11 +319,9 @@
    1.37    init_obj    :: "prog \<Rightarrow> obj_tag \<Rightarrow> oref \<Rightarrow> st \<Rightarrow> st"
    1.38   "init_obj G oi r \<equiv> gupd(r\<mapsto>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>)"
    1.39  
    1.40 -syntax
    1.41 +abbreviation
    1.42    init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
    1.43 -
    1.44 -translations
    1.45 - "init_class_obj G C" == "init_obj G CONST undefined (CONST Inr C)"
    1.46 +  where "init_class_obj G C == init_obj G undefined (Inr C)"
    1.47  
    1.48  lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
    1.49  apply (unfold gupd_def)
    1.50 @@ -513,19 +505,17 @@
    1.51  apply auto
    1.52  done
    1.53  
    1.54 -syntax
    1.55 +abbreviation raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
    1.56 +  where "raise_if c xn == abrupt_if c (Some (Xcpt (Std xn)))"
    1.57 +
    1.58 +abbreviation np :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
    1.59 +  where "np v == raise_if (v = Null) NullPointer"
    1.60  
    1.61 -  raise_if :: "bool \<Rightarrow> xname \<Rightarrow> abopt \<Rightarrow> abopt"
    1.62 -  np       :: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
    1.63 -  check_neg:: "val  \<spacespace>        \<Rightarrow> abopt \<Rightarrow> abopt"
    1.64 -  error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt"
    1.65 -  
    1.66 -translations
    1.67 +abbreviation check_neg :: "val \<Rightarrow> abopt \<Rightarrow> abopt"
    1.68 +  where "check_neg i' == raise_if (the_Intg i'<0) NegArrSize"
    1.69  
    1.70 - "raise_if c xn" == "abrupt_if c (Some (Xcpt (Std xn)))"
    1.71 - "np v"          == "raise_if (v = Null)      NullPointer"
    1.72 - "check_neg i'"  == "raise_if (the_Intg i'<0) NegArrSize"
    1.73 - "error_if c e"  == "abrupt_if c (Some (Error e))"
    1.74 +abbreviation error_if :: "bool \<Rightarrow> error \<Rightarrow> abopt \<Rightarrow> abopt"
    1.75 +  where "error_if c e == abrupt_if c (Some (Error e))"
    1.76  
    1.77  lemma raise_if_None [simp]: "(raise_if c x y = None) = (\<not>c \<and> y = None)"
    1.78  apply (simp add: abrupt_if_def)
    1.79 @@ -592,22 +582,23 @@
    1.80  types
    1.81    state = "abopt \<times> st"          --{* state including abruption information *}
    1.82  
    1.83 -syntax 
    1.84 -  Norm   :: "st \<Rightarrow> state"
    1.85 -  abrupt :: "state \<Rightarrow> abopt"
    1.86 -  store  :: "state \<Rightarrow> st"
    1.87 -
    1.88  translations
    1.89 -   
    1.90 -  "Norm s"     == "(None,s)" 
    1.91 -  "abrupt"     => "fst"
    1.92 -  "store"      => "snd"
    1.93    "abopt"       <= (type) "State.abrupt option"
    1.94    "abopt"       <= (type) "abrupt option"
    1.95    "state"      <= (type) "abopt \<times> State.st"
    1.96    "state"      <= (type) "abopt \<times> st"
    1.97  
    1.98 +abbreviation
    1.99 +  Norm :: "st \<Rightarrow> state"
   1.100 +  where "Norm s == (None, s)"
   1.101  
   1.102 +abbreviation (input)
   1.103 +  abrupt :: "state \<Rightarrow> abopt"
   1.104 +  where "abrupt == fst"
   1.105 +
   1.106 +abbreviation (input)
   1.107 +  store :: "state \<Rightarrow> st"
   1.108 +  where "store == snd"
   1.109  
   1.110  lemma single_stateE: "\<forall>Z. Z = (s::state) \<Longrightarrow> False"
   1.111  apply (erule_tac x = "(Some k,y)" in all_dupE)
   1.112 @@ -683,15 +674,11 @@
   1.113  lemma supd_abrupt_invariant [simp]: "abrupt (supd f s) = abrupt s"
   1.114    by (cases s) simp
   1.115  
   1.116 -syntax
   1.117 +abbreviation set_lvars :: "locals \<Rightarrow> state \<Rightarrow> state"
   1.118 +  where "set_lvars l == supd (set_locals l)"
   1.119  
   1.120 -  set_lvars     :: "locals \<Rightarrow> state \<Rightarrow> state"
   1.121 -  restore_lvars :: "state  \<Rightarrow> state \<Rightarrow> state"
   1.122 -  
   1.123 -translations
   1.124 -
   1.125 - "set_lvars l" == "supd (set_locals l)"
   1.126 - "restore_lvars s' s" == "set_lvars (locals (store s')) s"
   1.127 +abbreviation restore_lvars :: "state  \<Rightarrow> state \<Rightarrow> state"
   1.128 +  where "restore_lvars s' s == set_lvars (locals (store s')) s"
   1.129  
   1.130  lemma set_set_lvars [simp]: "\<And> s. set_lvars l (set_lvars l' s) = set_lvars l s"
   1.131  apply (simp (no_asm_simp) only: split_tupled_all)