src/HOL/IMPP/Misc.thy
changeset 17477 ceb42ea2f223
parent 8177 e59e93ad85eb
child 19803 aa2581752afb
equal deleted inserted replaced
17476:315cb57e3dd7 17477:ceb42ea2f223
     1 (*  Title:      HOL/IMPP/Misc.thy
     1 (*  Title:      HOL/IMPP/Misc.thy
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     David von Oheimb
     3     Author:     David von Oheimb
     4     Copyright   1999 TUM
     4     Copyright   1999 TUM
       
     5 *)
     5 
     6 
     6 Several examples for Hoare logic
     7 header {* Several examples for Hoare logic *}
     7 *)
     8 
     8 Misc = Hoare +
     9 theory Misc
       
    10 imports Hoare
       
    11 begin
     9 
    12 
    10 defs
    13 defs
    11   newlocs_def "newlocs       == %x. arbitrary"
    14   newlocs_def: "newlocs       == %x. arbitrary"
    12   setlocs_def "setlocs s l'  == case s of st g l => st g l'"
    15   setlocs_def: "setlocs s l'  == case s of st g l => st g l'"
    13   getlocs_def "getlocs s     == case s of st g l => l"
    16   getlocs_def: "getlocs s     == case s of st g l => l"
    14    update_def "update s vn v == case vn of
    17    update_def: "update s vn v == case vn of
    15                               Glb gn => (case s of st g l => st (g(gn:=v)) l)
    18                                Glb gn => (case s of st g l => st (g(gn:=v)) l)
    16                             | Loc ln => (case s of st g l => st g (l(ln:=v)))"
    19                              | Loc ln => (case s of st g l => st g (l(ln:=v)))"
       
    20 
       
    21 ML {* use_legacy_bindings (the_context ()) *}
    17 
    22 
    18 end
    23 end
    19