# Theory DSWMark

section ‹Deutsch-Schorr-Waite Marking Algorithm›

theory DSWMark
begin

text‹
Finally, we construct the Deutsch-Schorr-Waite marking algorithm by assuming that there
are only two pointers ($\mathit{left}$, $\mathit{right}$) from every node. There is also a new variable,
$\mathit{atom}: \mathit{node} \to \mathit{bool}$ which associates to every node a Boolean value.
The data invariant of this refinement step requires that $\mathit{index}$ has exactly two distinct
elements $none$  and $\mathit{some}$, $\mathit{left} = \mathit{link}\ \mathit{none}$,
$\mathit{right}=\mathit{link}\ \mathit{some}$, and $\mathit{atom}\ x$ is true
if and only if $\mathit{label}\ x = \mathit{some}$.

We use a new locale which fixes the initial values of the variables $\mathit{left}$, $\mathit{right}$, and
$\mathit{atom}$ in $\mathit{left0}$, $\mathit{right0}$, and $\mathit{atom0}$ respectively.
›

datatype Index = none | some

locale classical = node +
fixes left0  :: "'node ⇒ 'node"
fixes right0 :: "'node ⇒ 'node"
fixes atom0  :: "'node ⇒ bool"
assumes "(nil::'node) = nil"
begin
definition
"link0 i = (if i = (none::Index) then left0 else right0)"

definition
"label0 x = (if atom0 x then (some::Index) else none)"
end

sublocale classical ⊆ dsw?: pointer "nil" "root" "none::Index" "link0" "label0"
proof qed auto

context classical
begin

lemma [simp]:
"(label0 = (λ x . if atom x then some else none)) = (atom0 = atom)"
by auto

definition
"gg mrk atom ptr x ≡ ptr x ≠ nil ∧ ptr x ∉ mrk ∧ ¬ atom x"

subsection ‹Transitions›

definition
"QQ1_a ≡ [: p, t, left, right, atom, mrk ↝ p', t', left', right', atom', mrk' .
root = nil ∧  p' = nil ∧ t' = nil ∧ mrk' = mrk ∧ left' = left
∧ right' = right ∧ atom' = atom :]"

definition
"QQ2_a ≡ [: p, t, left, right, atom, mrk ↝ p', t', left', right', atom', mrk' .
root ≠ nil ∧  p' = root ∧ t' = nil ∧ mrk' = mrk ∪ {root}
∧ left' = left ∧ right' = right ∧ atom' = atom :]"

definition
"QQ3_a ≡ [: p, t, left, right, atom, mrk ↝ p', t', left', right', atom', mrk' .
p ≠ nil ∧ gg mrk atom left p ∧
p' = left p ∧ t' = p ∧ mrk' = mrk ∪ {left p} ∧
left' = left(p := t) ∧ right' = right ∧ atom' = atom:]"

definition
"QQ4_a ≡ [: p, t, left, right, atom, mrk ↝ p', t', left', right', atom', mrk' .
p ≠ nil ∧ gg mrk atom right p ∧
p' = right p ∧ t' = p ∧ mrk' = mrk ∪ {right p} ∧
left' = left ∧ right' = right(p := t) ∧ atom' = atom(p := True) :]"

definition
"QQ5_a ≡ [: p, t, left, right, atom, mrk ↝ p', t', left', right', atom', mrk' .
p ≠ nil ∧ ― ‹not needed in the proof›
¬ gg mrk atom left p ∧ ¬ gg mrk atom right p ∧
t ≠ nil ∧ ¬ atom t ∧
p' = t ∧ t' = left t ∧ mrk' = mrk ∧
left' = left(t := p) ∧ right' = right ∧ atom' = atom :]"

definition
"QQ6_a ≡ [: p, t, left, right, atom, mrk ↝ p', t', left', right', atom', mrk' .
p ≠ nil ∧ ― ‹not needed in the proof›
¬ gg mrk atom left p ∧ ¬ gg mrk atom right p ∧
t ≠ nil ∧ atom t ∧
p' = t ∧ t' = right t ∧ mrk' = mrk ∧
left' = left ∧ right' = right(t := p) ∧ atom' = atom(t := False) :]"

definition
"QQ7_a ≡ [: p, t, left, right, atom, mrk ↝ p', t', left', right', atom', mrk' .
p ≠ nil ∧
¬ gg mrk atom left p ∧ ¬ gg mrk atom right p ∧
t = nil ∧
p' = nil ∧ t' = t ∧ mrk' = mrk ∧
left' = left ∧ right' = right ∧ atom' = atom :]"

definition
"QQ8_a ≡ [: p, t, left, right, atom, mrk ↝ p', t', left', right', atom', mrk' .
p = nil ∧ p' = p ∧ t' = t ∧ mrk' = mrk ∧ left' = left ∧ right' = right ∧ atom' = atom:]"

section ‹Data refinement relation›

definition
"RR_a ≡ {: p, t, left, right, atom, mrk ↝ p', t', lnk, lbl, mrk' .
lnk none = left ∧ lnk some = right ∧
lbl = (λ x . if atom x then some else none) ∧
p' = p ∧ t' = t ∧ mrk' = mrk :}"

definition [simp]:
"R''_a i = RR_a"

definition
"ClassicMark = (λ (i, j) . (case (i, j) of
(I.init, I.loop)  ⇒ QQ1_a ⊓ QQ2_a |
(I.loop, I.loop)  ⇒ (QQ3_a ⊓ QQ4_a) ⊓ ((QQ5_a ⊓ QQ6_a) ⊓ QQ7_a) |
(I.loop, I.final) ⇒ QQ8_a |
_ ⇒ ⊤))"

subsection ‹Data refinement of the transitions›

theorem init1_a [simp]:
"DataRefinement ({.Init''.} o Q1''_a) RR_a RR_a QQ1_a"
by (simp add: data_refinement_hoare hoare_demonic angelic_def QQ1_a_def Q1''_a_def RR_a_def
Init''_def subset_eq)

theorem init2_a [simp]:
"DataRefinement ({.Init''.} o Q2''_a) RR_a RR_a QQ2_a"
by (simp add: data_refinement_hoare hoare_demonic angelic_def QQ2_a_def Q2''_a_def RR_a_def
Init''_def subset_eq)

lemma index_simp:
"(u = v) = (u none = v none ∧ u some = v some)"
by (safe, rule ext, case_tac "x", auto)

theorem step1_a [simp]:
"DataRefinement ({.Loop''.} o Q3''_a) RR_a RR_a QQ3_a"
apply (simp add: data_refinement_hoare hoare_demonic angelic_def QQ3_a_def  Q3''_a_def RR_a_def
Loop''_def subset_eq g_def gg_def simp_eq_emptyset)
apply safe
apply (rule_tac x="λ x . if x = some then ab some else (ab none)(a := aa)" in exI)
apply simp
apply (rule_tac x="none" in exI)
done

theorem step2_a[simp]:
"DataRefinement ({.Loop''.} o Q3''_a) RR_a RR_a QQ4_a"
apply (simp add: data_refinement_hoare hoare_demonic angelic_def QQ4_a_def Q3''_a_def RR_a_def
Loop''_def subset_eq g_def gg_def simp_eq_emptyset)
apply safe
apply (rule_tac x="λ x . if x = none then ab none else (ab some)(a := aa)" in exI)
apply simp
apply (rule_tac x="some" in exI)
apply (rule ext)
apply auto
done

theorem step3_a [simp]:
"DataRefinement ({.Loop''.} o Q4''_a) RR_a RR_a QQ5_a"
apply (simp add: data_refinement_hoare hoare_demonic angelic_def QQ5_a_def Q4''_a_def RR_a_def
Loop''_def subset_eq g_def gg_def simp_eq_emptyset)
apply clarify
apply (case_tac "i")
apply auto
done

lemma if_set_elim: "(x ∈ (if b then A else B)) = ((b ∧ x ∈ A) ∨ (¬ b ∧ x ∈ B))"
by auto

theorem step4_a [simp]:
"DataRefinement ({.Loop''.} o  Q4''_a) RR_a RR_a QQ6_a"
apply (simp add: data_refinement_hoare hoare_demonic angelic_def RR_a_def QQ6_a_def Q4''_a_def
Loop''_def subset_eq simp_eq_emptyset g_def gg_def if_set_elim)
apply safe
apply (case_tac "i")
apply simp_all
apply (case_tac "i")
apply simp_all
apply (case_tac "i")
apply simp_all
apply (case_tac "i")
by simp_all

theorem step5_a [simp]:
"DataRefinement ({.Loop''.} o Q5''_a) RR_a RR_a QQ7_a"
apply (simp add: data_refinement_hoare hoare_demonic angelic_def Q5''_a_def QQ7_a_def
Loop''_def subset_eq RR_a_def simp_eq_emptyset)
apply safe
apply (case_tac "i")
by auto

theorem final_step_a [simp]:
"DataRefinement ({.Loop''.} o Q6''_a) RR_a RR_a QQ8_a"
by (simp add: data_refinement_hoare hoare_demonic angelic_def Q6''_a_def QQ8_a_def
Loop''_def subset_eq RR_a_def simp_eq_emptyset)

subsection ‹Diagram data refinement›

lemma [simp]: "mono RR_a" by (simp add: RR_a_def)
lemma [simp]: "RR_a ∈ Apply.Disjunctive" by (simp add: RR_a_def)
lemma [simp]: "Disjunctive_fun R''_a" by (simp add: Disjunctive_fun_def)

lemma [simp]: "mono_fun R''_a" by simp

lemma [simp]: "mono Q1''_a" by (simp add: Q1''_a_def)
lemma [simp]: "mono Q2''_a" by (simp add: Q2''_a_def)
lemma [simp]: "mono Q3''_a" by (simp add: Q3''_a_def)
lemma [simp]: "mono Q4''_a" by (simp add: Q4''_a_def)
lemma [simp]: "mono Q5''_a" by (simp add: Q5''_a_def)
lemma [simp]: "mono Q6''_a" by (simp add: Q6''_a_def)

by simp

theorem ClassicMark_DataRefinement_a [simp]:
"DgrDataRefinement2 (R'_a .. (R_a .. SetMarkInv)) LinkMark R''_a ClassicMark"
apply (rule_tac P = "LinkMarkInv" in DgrDataRefinement_mono)
angelic_def R1'_a_def R2'_a_def Init''_def Loop''_def Final''_def)
apply auto
demonic_sup_inf data_refinement_choice2 assert_comp_choice)
apply (rule data_refinement_choice2)
apply simp
apply (rule data_refinement_choice1)
apply simp_all
apply (rule data_refinement_choice2)
apply simp_all
apply (rule data_refinement_choice1)
by simp_all

subsection ‹Diagram corectness›

theorem ClassicMark_correct_a [simp]:
"Hoare_dgr  (R''_a .. (R'_a .. (R_a .. SetMarkInv)))  ClassicMark
((R''_a .. (R'_a ..(R_a .. SetMarkInv))) ⊓ (- grd (step ClassicMark)))"
apply (rule_tac D = "LinkMark" in Diagram_DataRefinement2)
apply auto

text ‹
We have proved the correctness of the final algorithm, but the pre and the post conditions
involve the angelic choice operator and they depend on all data refinement steps we
have used to prove the final diagram. We simplify these conditions and we show that
we obtained indead the corectness of the marking algorithm.

The predicate $\mathit{ClassicInit}$ which is true for the $\mathit{init}$ situation states that initially
the variables $\mathit{left}$, $\mathit{right}$, and $\mathit{atom}$ are equal to their initial values and also
that no node is marked.

The predicate $\mathit{ClassicFinal}$ which is true for the $final$ situation states that at the end
the values of the variables $\mathit{left}$, $\mathit{right}$, and $\mathit{atom}$ are again equal to their initial values
and the variable $mrk$ records all reachable nodes. The reachable nodes are defined using our initial
$\mathit{next}$ relation, however if we unfold all locale interpretations and definitions we see easeily
that a node $x$ is reachable if there is a path from $root$ to $x$ along $\mathit{left}$ and $\mathit{right}$ functions,
and all nodes in this path have the atom bit false.
›

definition
"ClassicInit = {(p, t, left, right, atom, mrk) .
atom = atom0 ∧ left = left0 ∧ right = right0 ∧
finite (- mrk) ∧ mrk = {}}"

definition
"ClassicFinal = {(p, t, left, right, atom, mrk) .
atom = atom0 ∧ left = left0 ∧ right = right0 ∧
mrk = reach root}"

theorem [simp]:
"ClassicInit ⊆ (RR_a (R1'_a (R1_a (SetMarkInv init))))"
apply (simp add: ClassicInit_def angelic_def RR_a_def R1'_a_def R1_a_def Init_def Init''_def)
apply safe
apply (unfold simp_eq_emptyset)

theorem [simp]:
"(RR_a (R1'_a (R1_a (SetMarkInv final)))) ≤ ClassicFinal"
apply (simp add: ClassicFinal_def angelic_def RR_a_def R1'_a_def R1_a_def
apply auto

text‹
The indexed predicate $\mathit{ClassicPre}$ is the precondition of the diagram, and since we are only interested
in starting the marking diagram in the $init$ situation we set
$\mathit{ClassicPre} \ loop = \mathit{ClassicPre} \ \mathit{final} = \emptyset$.
›

definition [simp]:
"ClassicPre i =  (case i of
I.init  ⇒ ClassicInit |
I.loop  ⇒ {} |
I.final ⇒ {})"

text‹
We are interested on the other hand that the marking diagram terminates only in the $\mathit{final}$ situation. In order to
achieve this we define the postcondition of the diagram as the indexed predicate $\mathit{ClassicPost}$ which is empty
on every situation except $final$.
›

definition [simp]:
"ClassicPost i =  (case i of
I.init  ⇒ {} |
I.loop  ⇒ {} |
I.final ⇒ ClassicFinal)"

lemma exists_or:
"(∃ x . p x ∨ q x) = ((∃ x . p x) ∨ (∃ x . q x))"
by auto

lemma [simp]:
"(- grd (step  ClassicMark)) init = {}"
apply safe
apply simp
apply (drule_tac x = loop in spec)
by (simp add: ClassicMark_def QQ1_a_def QQ2_a_def demonic_def)

lemma [simp]: "grd ⊤ = ⊥"

lemma [simp]:
"(- grd (step  ClassicMark)) loop = {}"
apply safe
apply simp
apply (frule_tac x = "final" in spec)
apply (drule_tac x = "loop" in spec)
apply (unfold ClassicMark_def QQ1_a_def QQ2_a_def QQ3_a_def QQ4_a_def QQ5_a_def QQ6_a_def QQ7_a_def QQ8_a_def)
apply simp
apply (case_tac "a ≠ nil")
by auto

text ‹
The final theorem states the correctness of the marking diagram with respect to the precondition
$\mathit{ClassicPre}$ and the postcondition $\mathit{ClassicPost}$, that is, if the diagram starts in the initial
situation, then it will terminate in the final situation, and it will mark all reachable nodes.
›

lemma [simp]: "mono QQ1_a" by (simp add: QQ1_a_def)
lemma [simp]: "mono QQ2_a" by (simp add: QQ2_a_def)
lemma [simp]: "mono QQ3_a" by (simp add: QQ3_a_def)
lemma [simp]: "mono QQ4_a" by (simp add: QQ4_a_def)
lemma [simp]: "mono QQ5_a" by (simp add: QQ5_a_def)
lemma [simp]: "mono QQ6_a" by (simp add: QQ6_a_def)
lemma [simp]: "mono QQ7_a" by (simp add: QQ7_a_def)
lemma [simp]: "mono QQ8_a" by (simp add: QQ8_a_def)

lemma [simp]: "dmono ClassicMark"
apply (unfold dmono_def ClassicMark_def)
by simp

theorem "⊨ ClassicPre {| pt ClassicMark |} ClassicPost"
apply (rule_tac P = "(R''_a .. (R'_a .. (R_a ..SetMarkInv)))" in hoare_pre)
apply (subst le_fun_def)
apply simp
apply (rule_tac Q = "((R''_a .. (R'_a .. (R_a .. SetMarkInv))) ⊓ (- grd (step ((ClassicMark)))))" in hoare_mono)