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