src/HOL/IMPP/Misc.thy
changeset 62145 5b946c81dfbf
parent 58963 26bf09b95dda
child 63167 0909deb8059b
     1.1 --- a/src/HOL/IMPP/Misc.thy	Mon Jan 11 21:20:44 2016 +0100
     1.2 +++ b/src/HOL/IMPP/Misc.thy	Mon Jan 11 21:21:02 2016 +0100
     1.3 @@ -8,13 +8,29 @@
     1.4  imports Hoare
     1.5  begin
     1.6  
     1.7 -defs
     1.8 -  newlocs_def: "newlocs       == %x. undefined"
     1.9 -  setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
    1.10 -  getlocs_def: "getlocs s     == case s of st g l => l"
    1.11 -   update_def: "update s vn v == case vn of
    1.12 -                               Glb gn => (case s of st g l => st (g(gn:=v)) l)
    1.13 -                             | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    1.14 +overloading
    1.15 +  newlocs \<equiv> newlocs
    1.16 +  setlocs \<equiv> setlocs
    1.17 +  getlocs \<equiv> getlocs
    1.18 +  update \<equiv> update
    1.19 +begin
    1.20 +
    1.21 +definition newlocs :: locals
    1.22 +  where "newlocs == %x. undefined"
    1.23 +
    1.24 +definition setlocs :: "state => locals => state"
    1.25 +  where "setlocs s l' == case s of st g l => st g l'"
    1.26 +
    1.27 +definition getlocs :: "state => locals"
    1.28 +  where "getlocs s == case s of st g l => l"
    1.29 +
    1.30 +definition update  :: "state => vname => val => state"
    1.31 +  where "update s vn v ==
    1.32 +    case vn of
    1.33 +      Glb gn => (case s of st g l => st (g(gn:=v)) l)
    1.34 +    | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    1.35 +
    1.36 +end
    1.37  
    1.38  
    1.39  subsection "state access"