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^\<star>]Φ = (Φ ∧ [P][P^\<star>]Φ)"
  by (metis dBox_choice dBox_seq dBox_skip ustar_unfoldl)

lemma dBox_star_induct: "`(Φ ∧ [P<sup>\</sup><star>](Φ → [P]Φ)) → [P<sup>\</sup><star>]Φ`"
  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^\<star>]Φ"
  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