section ‹Generalization of Deutsch-Schorr-Waite Algorithm›

imports StackMark
begin

text ‹
In the third step the stack diagram is refined to a diagram where no extra
memory is used. The relation $next$  is replaced by two new variables $link$ and $label$.
The variable $\mathit{label}:\mathit{node}\to \mathit{index}$ associates a label to every node and the variable
$\mathit{link}: \mathit{index}\to \mathit{node}\to \mathit{node}$ is a collection of pointer functions indexed by the set
$\mathit{index}$ of labels. For $x\in \mathit{node}$, $\mathit{link} \ i \ x$ is the successor node of $x$  along
the function $\mathit{link} \ i$. In this context a node $x$ is reachable if there exists a path
from the root to $x$  along the links $\mathit{link} \ i$  such that all nodes in this path are
not $\mathit{nil}$ and they are labeled by a special label $\mathit{none}\in \mathit{index}$.

The stack variable $S$ is replaced by two new variables $p$ and $t$ ranging over nodes. Variable $p$
stores the head of $S$,  $t$ stores the head of the tail of $S$, and the rest of $S$
is stored by temporarily modifying the variables $\mathit{link}$ and $\mathit{label}$.

This algorithm is a generalization of the Deutsch-Schorr-Waite graph marking algorithm because
we have a collection of pointer functions instead of left and right only.
›

locale pointer = node +
fixes none :: "'index"
fixes link0::"'index ⇒ 'node ⇒ 'node"
fixes label0 :: "'node ⇒ 'index"
(* next assume is used to bind the type variable 'node introduced in this locale to the
type variable 'node introduced in the locale node. *)
assumes "(nil::'node) = nil"
begin
definition "next =  {(a, b) . (∃ i . link0 i a = b) ∧ a ≠ nil ∧ b ≠ nil ∧ label0 a = none}"
end

sublocale pointer ⊆ link?: graph "nil" "root" "next"
apply unfold_locales
apply (unfold next_def)
by auto

text‹
The locale pointer fixes the initial values for the variables $\mathit{link}$ and $\mathit{label}$ and
it defines the relation next as the union of all $\mathit{link} \ i$ functions, excluding
the mappings to $\mathit{nil}$, the mappings from $\mathit{nil}$ as well as the mappings from elements which
are not labeled by $\mathit{none}$.
›

text‹
The next two recursive functions, $\mathit{label}\_0$, $\mathit{link}\_0$ are used to compute
the initial values of the variables $\mathit{label}$ and $\mathit{link}$ from their current
values.
›

context pointer
begin
primrec
label_0:: "('node ⇒ 'index) ⇒ ('node list) ⇒ ('node ⇒ 'index)" where
"label_0 lbl []      = lbl" |
"label_0 lbl (x # l) = label_0 (lbl(x := none)) l"

lemma label_cong [cong]: "f = g ⟹ xs = ys ⟹ pointer.label_0 n f xs = pointer.label_0 n g ys"
by simp

primrec
link_0:: "('index ⇒ 'node ⇒ 'node) ⇒ ('node ⇒ 'index) ⇒ 'node ⇒ ('node list) ⇒ ('index ⇒ 'node ⇒ 'node)" where
"link_0 lnk lbl p []       = lnk" |
"link_0 lnk lbl p (x # l)  = link_0 (lnk((lbl x) := ((lnk (lbl x))(x := p)))) lbl x l"

text‹
The function $\mathit{stack}$ defined bellow is the main data refinement relation connecting
the stack from the abstract algorithm to its concrete representation by temporarily
modifying the variable $\mathit{link}$ and $\mathit{label}$.
›

primrec
stack:: "('index ⇒ 'node ⇒ 'node) ⇒ ('node ⇒ 'index) ⇒ 'node ⇒ ('node list) ⇒ bool" where
"stack lnk lbl x []       = (x = nil)" |
"stack lnk lbl x (y # l)  =
(x ≠ nil ∧ x = y ∧ ¬ x ∈ set l ∧ stack lnk lbl (lnk (lbl x) x) l)"

lemma label_out_range0 [simp]:
"¬ x ∈ set S ⟹ label_0 lbl S x = lbl x"
apply (rule_tac P="∀ label . ¬ x ∈ set S ⟶ label_0 label S x = label x" in mp)
by (simp, induct_tac S, auto)

"¬ x ∈ set S ⟹ link_0 link label p S i x = link i x"
apply (rule_tac P="∀ link p . ¬ x ∈ set S ⟶ link_0 link label p S i x = link i x" in mp)
by (simp, induct_tac S, auto)

by (simp, induct_tac S, auto)

lemma empty_stack [simp]: "stack link label nil S = (S = [])"
by (case_tac S, simp_all)

lemma stack_out_link_range [simp]: "¬ p ∈ set S ⟹ stack (link(i := (link i)(p := q))) label x S = stack link label x S"
apply (rule_tac P = "∀ link x . ¬ p ∈ set S ⟶ stack (link(i := (link i)(p := q))) label x S = stack link label x S" in mp)
by (simp, induct_tac S, auto)

lemma stack_out_label_range [simp]: "¬ p ∈ set S ⟹ stack link (label(p := q)) x S = stack link label x S"
apply (rule_tac P = "∀ link x . ¬ p ∈ set S ⟶ stack link (label(p := q)) x S = stack link label x S" in mp)
by (simp, induct_tac S, auto)

definition
"g mrk lbl ptr x ≡ ptr x ≠ nil ∧ ptr x ∉ mrk ∧ lbl x = none"

lemma g_cong [cong]: "mrk = mrk1 ⟹ lbl = lbl1 ⟹ ptr = ptr1 ⟹ x = x1 ==>
pointer.g n m mrk lbl ptr x = pointer.g n m mrk1 lbl1 ptr1 x1"
by simp

subsection ‹Transitions›

definition
"Q1''_a ≡ [: p, t, lnk, lbl, mrk ↝ p', t', lnk', lbl', mrk' .
root = nil ∧ p' = nil ∧ t' = nil ∧ lnk' = lnk ∧ lbl' = lbl ∧ mrk' = mrk:]"

definition
"Q2''_a ≡ [: p, t, lnk, lbl, mrk ↝ p', t', lnk', lbl', mrk' .
root ≠ nil ∧ p' = root ∧ t' = nil ∧ lnk' = lnk ∧ lbl' = lbl ∧ mrk' = mrk ∪ {root} :]"

definition
"Q3''_a ≡ [: p, t, lnk, lbl, mrk ↝ p', t', lnk', lbl', mrk' .
p ≠ nil ∧
(∃ i . g mrk lbl (lnk i) p ∧
p' = lnk i p ∧ t' =  p ∧ lnk' =  lnk(i := (lnk i)(p := t)) ∧ lbl' = lbl(p := i) ∧
mrk' = mrk ∪ {lnk i p}) :]"

definition
"Q4''_a  ≡ [: p, t, lnk, lbl, mrk ↝ p', t', lnk', lbl', mrk' .
p ≠ nil ∧
(∀ i . ¬ g mrk lbl (lnk i) p) ∧ t ≠ nil ∧
p' = t ∧ t' = lnk (lbl t) t ∧ lnk' = lnk(lbl t := (lnk (lbl t))(t := p))
∧ lbl' = lbl(t := none) ∧ mrk' = mrk:]"

definition
"Q5''_a ≡ [: p, t, lnk, lbl, mrk ↝ p', t', lnk', lbl', mrk' .
p ≠ nil ∧
(∀ i . ¬ g mrk lbl (lnk i) p) ∧ t = nil ∧
p' = nil ∧ t' = t ∧ lnk' =  lnk ∧ lbl' = lbl ∧ mrk' = mrk:]"

definition
"Q6''_a ≡ [: p, t, lnk, lbl, mrk ↝ p', t', lnk', lbl', mrk' . p = nil ∧
p' = p ∧ t' = t ∧ lnk' = lnk ∧ lbl' =  lbl ∧ mrk' = mrk :]"

subsection ‹Invariants›

definition
"Init'' ≡ { (p, t, lnk, lbl, mrk) . lnk = link0 ∧ lbl = label0}"

definition
"Loop'' ≡ UNIV"

definition
"Final'' ≡ Init''"

subsection ‹Data refinement relations›

definition
"R1'_a ≡ {: p, t, lnk, lbl, mrk ↝ stk, mrk' . (p, t, lnk, lbl, mrk) ∈ Init'' ∧ mrk' = mrk:}"

definition
"R2'_a ≡ {: p, t, lnk, lbl, mrk ↝ stk, mrk' .
t = head (tail stk) ∧
stack lnk lbl t (tail stk) ∧
label0 = label_0 lbl (tail stk) ∧
¬ nil ∈ set stk ∧
mrk' = mrk :}"

lemma [simp]: "R1'_a ∈ Apply.Disjunctive" by (simp add: R1'_a_def)

lemma [simp]: "R2'_a ∈ Apply.Disjunctive" by (simp add: R2'_a_def)

definition [simp]:
"R'_a i = (case i of
I.init  ⇒ R1'_a |
I.loop  ⇒ R2'_a |
I.final ⇒ R1'_a)"

lemma [simp]: "Disjunctive_fun R'_a" by (simp add: Disjunctive_fun_def)

subsection‹Diagram›

definition
"LinkMark = (λ (i, j) . (case (i, j) of
(I.init, I.loop)  ⇒ Q1''_a ⊓  Q2''_a |
(I.loop, I.loop)  ⇒ Q3''_a ⊓ (Q4''_a ⊓ Q5''_a) |
(I.loop, I.final) ⇒ Q6''_a |
_ ⇒ ⊤))"

definition [simp]:
"LinkMarkInv i = (case i of
I.init  ⇒ Init'' |
I.loop  ⇒ Loop'' |
I.final ⇒ Final'')"

subsection ‹Data refinement of the transitions›

theorem init1_a [simp]:
"DataRefinement ({.Init'.} o Q1'_a) R1'_a R2'_a Q1''_a"
by (simp add: data_refinement_hoare hoare_demonic Q1''_a_def Init'_def Init''_def
Loop''_def R1'_a_def R2'_a_def Q1'_a_def tail_def head_def angelic_def subset_eq)

theorem init2_a [simp]:
"DataRefinement ({.Init'.} o Q2'_a) R1'_a R2'_a Q2''_a"
by (simp add: data_refinement_hoare hoare_demonic Q2''_a_def Init'_def Init''_def
Loop''_def R1'_a_def R2'_a_def Q2'_a_def tail_def head_def angelic_def subset_eq)

theorem step1_a [simp]:
"DataRefinement ({.Loop'.} o Q3'_a) R2'_a R2'_a Q3''_a"
apply (simp add: data_refinement_hoare hoare_demonic Q3''_a_def Init'_def Init''_def
Loop'_def R1'_a_def Q3'_a_def tail_def head_def angelic_def subset_eq)
apply (unfold next_def)
apply (simp_all add: R2'_a_def angelic_def hoare_demonic simp_eq_emptyset)
apply auto
apply (rule_tac x = "aa i (hd a) # a" in exI)
apply safe
apply simp_all
apply clarify
apply (case_tac a)
apply (case_tac a)
apply simp_all
apply (case_tac a)
by auto

lemma neqif [simp]: "x ≠ y ⟹ (if y = x then a else b) = b"
apply (case_tac "y ≠ x")
apply simp_all
done

theorem step2_a [simp]:
"DataRefinement ({.Loop'.} o Q4'_a) R2'_a R2'_a Q4''_a"
apply (simp add: data_refinement_hoare hoare_demonic Q4''_a_def Init'_def Init''_def
Loop'_def Q4'_a_def tail_def head_def angelic_def subset_eq)
apply (unfold next_def)
apply (simp_all add: R2'_a_def angelic_def hoare_demonic simp_eq_emptyset)
apply (unfold g_def)
apply safe
apply auto [1]
apply auto [1]
apply (case_tac ysa)
apply simp_all
apply safe
apply (case_tac "ab ya = i")
by auto

lemma setsimp: "a = c ⟹ (x ∈ a) = (x ∈ c)"
apply simp
done

theorem step3_a [simp]:
"DataRefinement ({.Loop'.} o Q4'_a) R2'_a R2'_a Q5''_a"
apply (simp add: data_refinement_hoare hoare_demonic Q5''_a_def Init'_def Init''_def
Loop'_def Q4'_a_def angelic_def subset_eq)
apply (unfold R2'_a_def)
apply (unfold next_def)
apply (simp add: data_refinement_hoare hoare_demonic angelic_def subset_eq
by auto

theorem final_a [simp]:
"DataRefinement ({.Loop'.} o Q5'_a) R2'_a R1'_a Q6''_a"
apply (simp add: data_refinement_hoare hoare_demonic Q6''_a_def Init'_def Init''_def
Loop'_def R2'_a_def R1'_a_def Q5'_a_def angelic_def subset_eq neq_Nil_conv tail_def head_def)
apply safe
by simp_all

subsection ‹Diagram data refinement›

lemma apply_fun_index [simp]: "(r .. P) i = (r i) (P i)" by (simp add: apply_fun_def)

lemma [simp]: "Disjunctive_fun (r::('c ⇒ 'a::complete_lattice ⇒ 'b::complete_lattice))
⟹ mono_fun r"

"DgrDataRefinement2 (R_a .. SetMarkInv) StackMark_a R'_a LinkMark"
apply (rule_tac P = "StackMarkInv" in DgrDataRefinement_mono)
apply (simp add: le_fun_def SetMarkInv_def angelic_def
R1_a_def R2_a_def Init'_def Final'_def)
apply safe
apply simp
StackMark_a_def demonic_sup_inf data_refinement_choice2 assert_comp_choice)
apply (rule data_refinement_choice2)
apply simp_all
apply (rule data_refinement_choice1)
by simp_all

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]: "dmono StackMark_a"
apply (unfold dmono_def StackMark_a_def)
by simp

subsection ‹Diagram correctness›