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