Theory State

Up to index of Isabelle/HOL/Marvin2002

(* 
    File:        /home/hemer/RefLP/Marvin/State.thy
    Theory Name: State
    Logic Image: HOL
*)

State  =  Command + PartComp + Map + Fun +

types
  State = "Bnds set"
end

theorem Exec_witness:

  empty({}|->{})
  : {e. dom e = Pow {b. {b} : dom e} &
        (ALL s:dom e. the (e s) <= s) &
        (ALL s:dom e. e s = Some {b. b : s & e {b} = Some {b}})}