Theory Execs

Up to index of Isabelle/HOL/Marvin99-1

Execs = Command + Pointwise + RefRels + PartComp + State +

types
  StateMap = "State ~=> State" 
typedef
  Exec = "{(e :: State ~=> State) . (dom(e) = (Pow {b. {b}:dom(e)}))
           & ( ! s:dom e. the (e s) <= s)
           & (! s: dom(e). e(s) =  Some {b. b:s & (e({b}) = Some {b})})}"
  (Exec_witness)
types
  PExec = "rterm => Exec"
  Env = "PIdent ~=> PCmd"
  Ctx = "PExec => PExec"
consts 
  exec  :: "[Env,Cmd] => StateMap" 
  unbind :: "[Var, State] => State"
  ex     :: "[Var, StateMap] => StateMap"
  forall    :: "[Var, StateMap] => StateMap"
  assign :: "[Var, rterm] => State =>  State"
  pexec :: "[Env,PCmd] => PExec"
primrec
  "exec p (spec x) = (%s . Some (s Int bnds(x)))" 
  "exec p (assert x) = (%s . if  s <= bnds(x)  then Some s else None)" 
  "exec p (c1 pand c2) = ((exec p c1) PInt (exec p c2))"        
  "exec p (c1 por c2) = ((exec p c1) PUn (exec p c2))"
  "exec p (c1 sand c2) = ((exec p c1) o; (exec p c2))" 
  "exec p (exists v c) = ex v (exec p c)"
  "exec p (Cmd.all v c) = forall v (exec p c)"
  "exec p fail  = (%s. Some {})"
  "exec p abort = (%s. if s = {} then Some {} else None)"  
  "exec p (pcall fid t) =
   (if fid: dom(p)
    then Rep_Exec(pexec (p(fid:=None)) (the (p fid))(t))
    else (%s. if s = {} then Some {} else None))"
defs
  unbind_def "unbind v s == {b1. ? b:s. ? x . b1 = (b (v:=x))}"
  ex_def "ex v e == (%s. if (unbind v s:dom e)
                     then Some ({b. b:s & (? x. 
                                           (e({b(v:=x)})) ~= Some {})})
                     else None)" 

  forall_def "forall v e == (%s. if (unbind v s:dom e) 
                             then Some({b. b:s
                                        & (! x. (e({b(v:=x)})) ~= Some {})})
                             else None)"
  assign_def "assign v t == (%s. {b1 . ? b:s . b1 = b(v := eval t b)})"

rules
  exec_property1 "dom(exec p c) = Pow {b. {b}:dom(exec p c)}"
  exec_property3 "! s:dom(exec p c).
                  (exec p c)(s) = Some {b. b:s & ((exec p c)({b}) = Some {b})}"
  refsto_exec "((e1::StateMap) refsto e2)
               = ((dom(e1) <= dom(e2)) &
                  (! s: dom(e1). e1(s) = e2(s)))"                      
  refeq_exec "((e1::StateMap) refeq e2) = ((e1) = (e2))"
  refsto_pexec "((p1::PExec) refsto p2) = (! t. Rep_Exec (p1 t) refsto Rep_Exec (p2 t))"
  refeq_pexec "((p1::PExec) refeq p2) = (! t. Rep_Exec (p1 t) refeq Rep_Exec (p2 t))"
end

theorem id_in_MCtx:

  id : {C. ALL p q. p refsto q --> C p refsto C q}

theorem dom_assume:

  dom (exec p (assert A)) = {s. s <= bnds A}

theorem dom_pand:

  dom (exec p (c1 pand c2)) = dom (exec p c1) Int dom (exec p c2)

theorem assume_property1:

  dom (exec p (assert A)) = Pow {b. {b} : dom (exec p (assert A))}

theorem pand_property1:

  [| dom (exec p c1) = Pow {b. {b} : dom (exec p c1)};
     dom (exec p c2) = Pow {b. {b} : dom (exec p c2)} |]
  ==> dom (exec p (c1 pand c2)) = Pow {b. {b} : dom (exec p (c1 pand c2))}

theorem dom_exists:

  dom (exec p (exists v c)) = {s. unbind v s : dom (exec p c)}

theorem dom_all:

  dom (exec p (Cmd.all v c)) = {s. unbind v s : dom (exec p c)}

theorem dom_abort:

  dom (exec p abort) = {{}}

theorem exec_property2:

  ALL s:dom (exec p c). the (exec p c s) <= s

theorem exec_empty:

  exec p c {} = Some {}