Theory RefPoint

Up to index of Isabelle/HOL/Marvin99-1

RefPoint = RefAssume +

consts
  refeq_point :: "[Cmd,Env,Cmd] => pred"
  refsto_point :: "[Cmd,Env,Cmd] => pred"
rules
  refeq_point_def
  "evalp (refeq_point c1 p c2) b =
   ((exec p c1)({b}) = (exec p c2)({b}))"
  refsto_point_def
  "evalp (refsto_point c1 p c2) b = ({b}:dom(exec p c1)
   --> ((exec p c1)({b}) = (exec p c2)({b})))"
rules
  introduce_recursion
  "pc prefeq(p)
     ( re pid . (V :- (assert(pall y (refsto_point (assert(varT y << varT V) sand (pc ^@ varT y)) p (pcall pid (varT y))))) sand (pc ^@ (varT V))) er )"
  intro_recursion
  "env p ass (pall y (refsto_point (assert(varT y << varT V) sand (pc ^@ varT y)) p (pcall pid (varT y)))) ||- (pc ^@ (varT V)) [= C(pid) ==> pc prefeq(p) (re pid . V :- C(pid) er)"
    intro_recursion2
  "env p(pid:=Some (y :- assert(varT y << varT V) sand (pc ^@ varT y))) ass ptrue ||- (pc ^@ (varT V)) [= C(pid) ==> pc prefeq(p) (re pid . V :- C(pid) er)"
  substp_refsto_point "substp (refsto_point c1 p c2) v t  = (refsto_point
                (substC c1 v t) p (substC c2 v t))"
  syntax (symbols)
  "refsto_point" :: "[Cmd, Env, Cmd] => pred" ("_ \<sqsubseteq>'(_') _")
  "refeq_point" :: "[Cmd, Env, Cmd] => pred" ("_  [=]'(_') _")
(* consts
  crefeq :: "[Env,pred,Cmd,Cmd] => bool" ("env _ ass _ ||- _ [=] _")
  crefsto :: "[Env,pred,Cmd,Cmd] => bool" ("env _ ass _ ||- _ [= _")
defs
  crefeq_def "env p ass A ||- c1 [=] c2 == entails A (refeq_point c1 p c2)"
  crefsto_def "env p ass A ||- c1 [= c2 == entails A (refsto_point c1 p c2)" *)
end