# Theory DataRefinementIBP.Statements

section ‹Program Statements as Predicate Transformers›

theory Statements
imports Preliminaries
begin

text ‹
Program statements are modeled as predicate transformers, functions from predicates to predicates.
If $\mathit{State}$ is the type of program states, then a program $S$ is a a function from
$\mathit{State}\ \mathit{set}$ to
$\mathit{State}\ \mathit{set}$. If $q \in \mathit{State}\ \mathit{set}$, then the elements of
$S\ q$ are the initial states from which
$S$ is guarantied to terminate in a state from $q$.

However, most of the time we will work with an arbitrary compleate lattice, or an arbitrary boolean algebra
instead of the complete boolean algebra of predicate transformers.

We will introduce in this section assert, assume, demonic choice, angelic choice, demonic update, and
angelic update statements. We will prove also that these statements are monotonic.
›

lemma mono_top[simp]: "mono top"

lemma mono_choice[simp]: "mono S ⟹ mono T ⟹ mono (S ⊓ T)"
apply safe
apply (rule_tac y = "S x" in order_trans)
apply simp_all
apply (rule_tac y = "T x" in order_trans)
by simp_all

subsection "Assert statement"

text ‹
The assert statement of a predicate $p$ when executed from a state $s$ fails
if $s\not\in p$ and behaves as skip otherwise.
›

definition
assert::"'a::semilattice_inf ⇒ 'a ⇒ 'a" ("{. _ .}" [0] 1000) where
"{.p.} q ≡  p ⊓ q"

lemma mono_assert [simp]: "mono {.p.}"
apply (simp add: assert_def mono_def, safe)
apply (rule_tac y = "x" in order_trans)
by simp_all

subsection "Assume statement"

text ‹
The assume statement of a predicate $p$ when executed from a state $s$ is not enabled
if $s\not\in p$ and behaves as skip otherwise.
›

definition
"assume" :: "'a::boolean_algebra ⇒ 'a ⇒ 'a" ("[. _ .]" [0] 1000) where
"[. p .] q ≡  -p ⊔ q"

lemma mono_assume [simp]: "mono (assume P)"
apply safe
apply (rule_tac y = "y" in order_trans)
by simp_all

subsection "Demonic update statement"

text ‹
The demonic update statement of a relation $Q: \mathit{State} \to \mathit{Sate} \to bool$,
when executed in a state $s$ computes nondeterministically a new state $s'$ such
$Q\ s \ s'$ is true. In order for this statement to be correct all
possible choices of $s'$ should be correct. If there is no state $s'$
such that $Q\ s \ s'$, then the demonic update of $Q$ is not enabled
in $s$.
›

definition
demonic :: "('a ⇒ 'b::ord) ⇒ 'b::ord ⇒ 'a set" ("[: _ :]" [0] 1000) where
"[:Q:] p = {s . Q s ≤ p}"

lemma mono_demonic [simp]: "mono [:Q:]"
by auto

theorem demonic_bottom:
"[:R:] (⊥::('a::order_bot)) = {s . (R s) = ⊥}"
apply (unfold demonic_def, safe, simp_all)
apply (rule antisym)
by auto

theorem demonic_bottom_top [simp]:
"[:(⊥::_::order_bot):]  = ⊤"
by (simp add: fun_eq_iff inf_fun_def sup_fun_def demonic_def top_fun_def bot_fun_def)

theorem demonic_sup_inf:
"[:Q ⊔ Q':] = [:Q:] ⊓ [:Q':]"
by (simp add: fun_eq_iff sup_fun_def inf_fun_def demonic_def, blast)

subsection "Angelic update statement"

text ‹
The angelic update statement of a relation $Q: \mathit{State} \to \mathit{State} \to \mathit{bool}$ is similar
to the demonic version, except that it is enough that at least for one choice $s'$, $Q \ s \ s'$
is correct. If there is no state $s'$
such that $Q\ s \ s'$, then the angelic update of $Q$ fails in $s$.
›

definition
angelic :: "('a ⇒ 'b::{semilattice_inf,order_bot}) ⇒ 'b ⇒ 'a set"
("{: _ :}" [0] 1000) where
"{:Q:} p = {s . (Q s) ⊓ p ≠ ⊥}"

syntax "_update" :: "patterns => patterns => logic => logic" ("_ ↝ _ . _" 0)
translations
"_update (_patterns x xs) (_patterns y ys) t" == "CONST id (_abs
(_pattern x xs) (_Coll (_pattern y ys) t))"
"_update x y t" == "CONST id (_abs x (_Coll y t))"

term "{: y, z ↝ x, z' . P x y z z' :}"

theorem angelic_bottom [simp]:
"angelic R ⊥  = {}"

theorem angelic_disjunctive [simp]:
"{:(R::('a ⇒ 'b::complete_distrib_lattice)):} ∈ Apply.Disjunctive"
by (simp add: Apply.Disjunctive_def angelic_def inf_Sup, blast)

subsection "The guard of a statement"

text ‹
The guard of a statement $S$ is the set of iniatial states from which $S$
is enabled or fails.
›

definition
"((grd S)::'a::boolean_algebra) = - (S bot)"

lemma grd_choice[simp]: "grd (S ⊓ T) = (grd S) ⊔ (grd T)"

lemma grd_demonic: "grd [:Q:] = {s . ∃ s' . s' ∈ (Q s) }"