Theory utp_dynlog

section ‹ Dynamic Logic ›

theory utp_dynlog
  imports utp_sequent utp_wp
begin

subsection ‹ Definitions ›

named_theorems dynlog_simp and dynlog_intro

definition dBox :: "'s hrel ⇒ 's upred ⇒ 's upred" (‹❙[_❙]_› [0,999] 999)
where [upred_defs]: "dBox A Φ = A wp Φ"

definition dDia :: "'s hrel ⇒ 's upred ⇒ 's upred" (‹❙<_❙>_› [0,999] 999)
where [upred_defs]: "dDia A Φ = (¬ ❙[A❙] (¬ Φ))"

subsection ‹ Box Laws ›

lemma dBox_false [dynlog_simp]: "❙[false❙]Φ = true"
  by (rel_auto)

lemma dBox_skip [dynlog_simp]: "❙[II❙]Φ = Φ"
  by (rel_auto)

lemma dBox_assigns [dynlog_simp]: "❙[⟨σ⟩⇩a❙]Φ = (σ † Φ)"
  by (simp add: dBox_def wp_assigns_r)

lemma dBox_choice [dynlog_simp]: "❙[P ⊓ Q❙]Φ = (❙[P❙]Φ ∧ ❙[Q❙]Φ)"
  by (rel_auto)

lemma dBox_seq: "❙[P ;; Q❙]Φ = ❙[P❙]❙[Q❙]Φ"
  by (simp add: dBox_def wp_seq_r)

lemma dBox_star_unfold: "❙[P⇧⋆❙]Φ = (Φ ∧ ❙[P❙]❙[P⇧⋆❙]Φ)"
  by (metis dBox_choice dBox_seq dBox_skip ustar_unfoldl)

lemma dBox_star_induct: "`(Φ ∧ ❙[P⇧⋆❙](Φ ⇒ ❙[P❙]Φ)) ⇒ ❙[P⇧⋆❙]Φ`"
  by (rel_simp, metis (mono_tags, lifting) mem_Collect_eq rtrancl_induct)

lemma dBox_test: "❙[?[p]❙]Φ = (p ⇒ Φ)"
  by (rel_auto)

subsection ‹ Diamond Laws ›

lemma dDia_false [dynlog_simp]: "❙<false❙>Φ = false"
  by (simp add: dBox_false dDia_def)

lemma dDia_skip [dynlog_simp]: "❙<II❙>Φ = Φ"
  by (simp add: dBox_skip dDia_def)

lemma dDia_assigns [dynlog_simp]: "❙<⟨σ⟩⇩a❙>Φ = (σ † Φ)"
  by (simp add: dBox_assigns dDia_def subst_not)

lemma dDia_choice: "❙<P ⊓ Q❙>Φ = (❙<P❙>Φ ∨ ❙<Q❙>Φ)"
  by (simp add: dBox_def dDia_def wp_choice)

lemma dDia_seq: "❙<P ;; Q❙>Φ = ❙<P❙>❙<Q❙>Φ"
  by (simp add: dBox_def dDia_def wp_seq_r)

lemma dDia_test: "❙<?[p]❙>Φ = (p ∧ Φ)"
  by (rel_auto)

subsection ‹ Sequent Laws ›

lemma sBoxSeq [dynlog_simp]: "Γ ⊩ ❙[P ;; Q❙]Φ ≡ Γ ⊩ ❙[P❙]❙[Q❙]Φ"
  by (simp add: dBox_def wp_seq_r)

lemma sBoxTest [dynlog_intro]: "Γ ⊩ (b ⇒ Ψ) ⟹ Γ ⊩ ❙[?[b]❙]Ψ"
  by (rel_auto)

lemma sBoxAssignFwd [dynlog_simp]: "⟦ vwb_lens x; x ♯ v; x ♯ Γ ⟧ ⟹ (Γ ⊩ ❙[x := v❙]Φ) = ((&x =⇩u v ∧ Γ) ⊩ Φ)"
  by (rel_auto, metis vwb_lens_wb wb_lens.get_put)

lemma sBoxIndStar: "⊩ [Φ ⇒ ❙[P❙]Φ]⇩u ⟹ Φ ⊩ ❙[P⇧⋆❙]Φ"
  by (rel_simp, metis (mono_tags, lifting) mem_Collect_eq rtrancl_induct)

lemma hoare_as_dynlog: "⦃p⦄Q⦃r⦄⇩u = (p ⊩ ❙[Q❙]r)"
  by (rel_auto)

end