Theory Command

Up to index of Isabelle/HOL/Marvin2002

Command = Pred +

types
  PIdent = "string"
datatype Cmd = spec pred 
             | assert pred
             | pand Cmd Cmd (infixr 40)
             | por Cmd Cmd (infixr 40)
             | sand Cmd Cmd (infixr 40)
             | exists Var Cmd
             | all Var Cmd
             | fail
             | abort
             | pcall PIdent rterm

datatype PCmd = pcmd Var Cmd     ("_ :- _")
  | recblock PIdent PCmd         ("re _ . _ er")
  
consts
  freeVars :: "Cmd => Var set"
  substC :: "[Cmd, Var, rterm] => Cmd"
primrec
  "substC (spec P) v t = (spec (Pred.substp P v t))"
  "substC (assert P) v t = (assert (Pred.substp P v t))"
  "substC (S pand T) v t = ((substC S v t) pand (substC T v t))"
  "substC (S por T) v t = ((substC S v t) por (substC T v t))"
  "substC (S sand T) v t = ((substC S v t) sand (substC T v t))"
  "substC (exists U C) v t = (exists U (substC C v t))"
  "substC (Cmd.all U C) v t = (Cmd.all U (substC C v t))"
  "substC fail v t = (fail)"
  "substC abort v t = (abort)"
  "substC (pcall pid s) v t = (pcall pid (Term.substt s v t))"
syntax(symbols)
  "op pand" :: "[Cmd,Cmd] => Cmd" (infixr "\<and>" 35)
  "op por" :: "[Cmd, Cmd] => Cmd" (infixr "\<or>" 40)
(*  "op sand" :: "[Cmd, Cmd] => Cmd" (infixr "," 45)  *)
  "assert" :: "pred => Cmd" ("(1{_})") 
  "exists" :: "[Var, Cmd] => Cmd" ("(3\<exists> _./ _)" 10)
  syntax
  "@pcmd2" :: "[Var,Var,Cmd] => PCmd" ("(_, _) :- _")
end