Theory Recurse

Up to index of Isabelle/HOL/Marvin2002

Recurse = Execs +

typedef 
  MCtx = "{(C::Ctx) . ! p q . p refsto q --> C(p) refsto C(q)}" (id_in_MCtx)
consts 
  pexec :: "[Env,PCmd] => PExec"
  fix :: "MCtx => PExec"
  context :: "Env => PCmd => Ctx" 
primrec
  "context(env)(V :- c) = id"
primrec
  "pexec p (V :- c) =
   (%t. Abs_Exec (%s.
                  if (assign V t s: dom(exec p c))
                  then
                  Some({b. b:s
                        & (exec p c)(assign V t {b}) ~= Some {}})
                  else None))"
  "pexec p (re pid . pc er) =
   fix(Abs_MCtx (context(p)(re pid . pc er)))"
end