src/HOL/MicroJava/J/State.thy
changeset 35416 d8d7d1b785af
parent 35102 cc7a0b9f938c
child 42463 f270e3e18be5
     1.1 --- a/src/HOL/MicroJava/J/State.thy	Wed Feb 24 11:55:52 2010 +0100
     1.2 +++ b/src/HOL/MicroJava/J/State.thy	Mon Mar 01 13:40:23 2010 +0100
     1.3 @@ -14,11 +14,10 @@
     1.4  
     1.5    obj = "cname \<times> fields'"    -- "class instance with class name and fields"
     1.6  
     1.7 -constdefs
     1.8 -  obj_ty  :: "obj => ty"
     1.9 +definition obj_ty :: "obj => ty" where
    1.10   "obj_ty obj  == Class (fst obj)"
    1.11  
    1.12 -  init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)"
    1.13 +definition init_vars :: "('a \<times> ty) list => ('a \<rightharpoonup> val)" where
    1.14   "init_vars == map_of o map (\<lambda>(n,T). (n,default_val T))"
    1.15  
    1.16  types aheap  = "loc \<rightharpoonup> obj"    -- {* "@{text heap}" used in a translation below *}
    1.17 @@ -49,21 +48,19 @@
    1.18    lookup_obj :: "state \<Rightarrow> val \<Rightarrow> obj"
    1.19    where "lookup_obj s a' == the (heap s (the_Addr a'))"
    1.20  
    1.21 -
    1.22 -constdefs
    1.23 -  raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option"
    1.24 +definition raise_if :: "bool \<Rightarrow> xcpt \<Rightarrow> val option \<Rightarrow> val option" where
    1.25    "raise_if b x xo \<equiv> if b \<and>  (xo = None) then Some (Addr (XcptRef x)) else xo"
    1.26  
    1.27 -  new_Addr  :: "aheap => loc \<times> val option"
    1.28 +definition new_Addr  :: "aheap => loc \<times> val option" where
    1.29    "new_Addr h \<equiv> SOME (a,x). (h a = None \<and>  x = None) |  x = Some (Addr (XcptRef OutOfMemory))"
    1.30  
    1.31 -  np    :: "val => val option => val option"
    1.32 +definition np    :: "val => val option => val option" where
    1.33   "np v == raise_if (v = Null) NullPointer"
    1.34  
    1.35 -  c_hupd  :: "aheap => xstate => xstate"
    1.36 +definition c_hupd  :: "aheap => xstate => xstate" where
    1.37   "c_hupd h'== \<lambda>(xo,(h,l)). if xo = None then (None,(h',l)) else (xo,(h,l))"
    1.38  
    1.39 -  cast_ok :: "'c prog => cname => aheap => val => bool"
    1.40 +definition cast_ok :: "'c prog => cname => aheap => val => bool" where
    1.41   "cast_ok G C h v == v = Null \<or> G\<turnstile>obj_ty (the (h (the_Addr v)))\<preceq> Class C"
    1.42  
    1.43  lemma obj_ty_def2 [simp]: "obj_ty (C,fs) = Class C"