Quelle  utp_rel_opsem.thy

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 = (∀ σ₀ σ₁. `σ<sub>0</sub> † p` ∧ (σ₀, Q) →_u (σ₁, II) ⟶ `σ<sub>1</sub> † 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