Theory utp_rel_opsem

section ‹ Relational Operational Semantics ›

theory utp_rel_opsem
  imports 
    utp_rel_laws 
    utp_hoare
begin

text ‹ This theory uses the laws of relational calculus to create a basic operational semantics.
  It is based on Chapter 10 of the UTP book~\<^cite>‹"Hoare&98"›. ›
  
fun trel :: "'α usubst × 'α hrel ⇒ 'α usubst × 'α hrel ⇒ bool" (infix ‹→⇩u› 85) where
"(σ, P) →⇩u (ρ, Q) ⟷ (⟨σ⟩⇩a ;; P) ⊑ (⟨ρ⟩⇩a ;; Q)"

lemma trans_trel:
  "⟦ (σ, P) →⇩u (ρ, Q); (ρ, Q) →⇩u (φ, R) ⟧ ⟹ (σ, P) →⇩u (φ, R)"
  by auto

lemma skip_trel: "(σ, II) →⇩u (σ, II)"
  by simp

lemma assigns_trel: "(σ, ⟨ρ⟩⇩a) →⇩u (ρ ∘ σ, II)"
  by (simp add: assigns_comp)

lemma assign_trel:
  "(σ, x := v) →⇩u (σ(&x ↦⇩s σ † v), II)"
  by (simp add: assigns_comp usubst)

lemma seq_trel:
  assumes "(σ, P) →⇩u (ρ, Q)"
  shows "(σ, P ;; R) →⇩u (ρ, Q ;; R)"
  by (metis (no_types, lifting) assms order_refl seqr_assoc seqr_mono trel.simps)

lemma seq_skip_trel:
  "(σ, II ;; P) →⇩u (σ, P)"
  by simp

lemma nondet_left_trel:
  "(σ, P ⊓ Q) →⇩u (σ, P)"
  by (metis (no_types, opaque_lifting) disj_comm disj_upred_def semilattice_sup_class.sup.absorb_iff1 semilattice_sup_class.sup.left_idem seqr_or_distr trel.simps)

lemma nondet_right_trel:
  "(σ, P ⊓ Q) →⇩u (σ, Q)"
  by (simp add: seqr_mono)

lemma rcond_true_trel:
  assumes "σ † b = true"
  shows "(σ, P ◃ b ▹⇩r Q) →⇩u (σ, P)"
  using assms
  by (simp add: assigns_r_comp usubst alpha cond_unit_T)

lemma rcond_false_trel:
  assumes "σ † b = false"
  shows "(σ, P ◃ b ▹⇩r Q) →⇩u (σ, Q)"
  using assms
  by (simp add: assigns_r_comp usubst alpha cond_unit_F)

lemma while_true_trel:
  assumes "σ † b = true"
  shows "(σ, while b do P od) →⇩u (σ, P ;; while b do P od)"
  by (metis assms rcond_true_trel while_unfold)

lemma while_false_trel:
  assumes "σ † b = false"
  shows "(σ, while b do P od) →⇩u (σ, II)"
  by (metis assms rcond_false_trel while_unfold)

text ‹ Theorem linking Hoare calculus and operational semantics. If we start $Q$ in a state $\sigma_0$
  satisfying $p$, and $Q$ reaches final state $\sigma_1$ then $r$ holds in this final state. ›
    
theorem hoare_opsem_link:
  "⦃p⦄Q⦃r⦄⇩u = (∀ σ⇩0 σ⇩1. `σ⇩0 † p` ∧ (σ⇩0, Q) →⇩u (σ⇩1, II) ⟶ `σ⇩1 † r`)"
  apply (rel_auto)
  apply (rename_tac a b)
  apply (drule_tac x="λ _. a" in spec, simp)
  apply (drule_tac x="λ _. b" in spec, simp)
  done
    
declare trel.simps [simp del]

end