Theory utp_sym_eval

section ‹ Symbolic Evaluation of Relational Programs ›

theory utp_sym_eval
  imports utp_rel_opsem
begin

text ‹ The following operator applies a variable context $\Gamma$ as an assignment, and composes 
  it with a relation $P$ for the purposes of evaluation. ›

definition utp_sym_eval :: "'s usubst  's hrel  's hrel" (infixr "" 55) where
[upred_defs]: "utp_sym_eval Γ P = (Γa ;; P)"

named_theorems symeval

lemma seq_symeval [symeval]: "Γ  P ;; Q = (Γ  P) ;; Q"
  by (rel_auto)

lemma assigns_symeval [symeval]: "Γ  σa = (σ  Γ)  II"
  by (rel_auto)

lemma term_symeval [symeval]: "(Γ  II) ;; P = Γ  P"
  by (rel_auto)

lemma if_true_symeval [symeval]: " Γ  b = true   Γ  (P  b r Q) = Γ  P"
  by (simp add: utp_sym_eval_def usubst assigns_r_comp)

lemma if_false_symeval [symeval]: " Γ  b = false   Γ  (P  b r Q) = Γ  Q"
  by (simp add: utp_sym_eval_def usubst assigns_r_comp)

lemma while_true_symeval [symeval]: " Γ  b = true   Γ  while b do P od = Γ  (P ;; while b do P od)"
  by (subst while_unfold, simp add: symeval)

lemma while_false_symeval [symeval]: " Γ  b = false   Γ  while b do P od = Γ  II"
  by (subst while_unfold, simp add: symeval)

lemma while_inv_true_symeval [symeval]: " Γ  b = true   Γ  while b invr S do P od = Γ  (P ;; while b do P od)"
  by (metis while_inv_def while_true_symeval)

lemma while_inv_false_symeval [symeval]: " Γ  b = false   Γ  while b invr S do P od = Γ  II"
  by (metis while_false_symeval while_inv_def)

method sym_eval = (simp add: symeval usubst lit_simps[THEN sym]), (simp del: One_nat_def add: One_nat_def[THEN sym])?

syntax
  "_terminated" :: "logic  logic" ("terminated: _" [999] 999)

translations
  "terminated: Γ" == "Γ  II"

end