Theory utp_wp

section ‹Weakest (Liberal) Precondition Calculus›

theory utp_wp
imports utp_hoare
begin

text ‹A very quick implementation of wlp -- more laws still needed!›

named_theorems wp

method wp_tac = (simp add: wp)

consts
  uwp :: "'a ⇒ 'b ⇒ 'c" 

syntax
  "_uwp" :: "logic ⇒ uexp ⇒ logic" (infix ‹wp› 60)

syntax_consts
  "_uwp" == uwp

translations
  "_uwp P b" == "CONST uwp P b"

definition wp_upred :: "('α, 'β) urel ⇒ 'β cond ⇒ 'α cond" where
"wp_upred Q r = ⌊¬ (Q ;; (¬ ⌈r⌉⇩<)) :: ('α, 'β) urel⌋⇩<"

adhoc_overloading
  uwp wp_upred

declare wp_upred_def [urel_defs]

lemma wp_true [wp]: "p wp true = true"
  by (rel_simp)  
  
theorem wp_assigns_r [wp]:
  "⟨σ⟩⇩a wp r = σ † r"
  by rel_auto

theorem wp_skip_r [wp]:
  "II wp r = r"
  by rel_auto

theorem wp_abort [wp]:
  "r ≠ true ⟹ true wp r = false"
  by rel_auto

theorem wp_conj [wp]:
  "P wp (q ∧ r) = (P wp q ∧ P wp r)"
  by rel_auto

theorem wp_seq_r [wp]: "(P ;; Q) wp r = P wp (Q wp r)"
  by rel_auto

theorem wp_choice [wp]: "(P ⊓ Q) wp R = (P wp R ∧ Q wp R)"
  by (rel_auto)

theorem wp_cond [wp]: "(P ◃ b ▹⇩r Q) wp r = ((b ⇒ P wp r) ∧ ((¬ b) ⇒ Q wp r))"
  by rel_auto

lemma wp_USUP_pre [wp]: "P wp (⨆i∈{0..n} ∙ Q(i)) = (⨆i∈{0..n} ∙ P wp Q(i))"
  by (rel_auto)

theorem wp_hoare_link:
  "⦃p⦄Q⦃r⦄⇩u ⟷ (Q wp r ⊑ p)"
  by rel_auto

text ‹If two programs have the same weakest precondition for any postcondition then the programs
  are the same.›

theorem wp_eq_intro: "⟦ ⋀ r. P wp r = Q wp r ⟧ ⟹ P = Q"
  by (rel_auto robust, fastforce+)
end