Theory LinkMark

section ‹Generalization of Deutsch-Schorr-Waite Algorithm›

theory LinkMark
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)

lemma link_out_range0 [simp]:
  "¬ 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)

lemma link_out_range [simp]: "¬ x ∈ set S ⟹ link_0 link (label(x := y)) p S = link_0 link label p S"
  apply (rule_tac P="∀ link p . ¬ x ∈ set S ⟶ link_0 link (label(x := y)) p S = link_0 link label p S" in mp)
  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' .  
       p = head stk ∧  
       t = head (tail stk) ∧  
       stack lnk lbl t (tail stk) ∧ 
       link0 = link_0 lnk lbl p (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 add: R2'_a_def)
  apply (simp add: data_refinement_hoare)
  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 (simp add: g_def  neq_Nil_conv)
  apply clarify
  apply (simp add: g_def  neq_Nil_conv)
  apply (case_tac a)
  apply (simp_all add: g_def  neq_Nil_conv)
  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 add: R2'_a_def)
  apply (simp add: data_refinement_hoare)
  apply (simp_all add: R2'_a_def angelic_def hoare_demonic simp_eq_emptyset)
  apply (simp_all add: neq_Nil_conv)
  apply (unfold g_def)
  apply (simp add: head_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 
           simp_eq_emptyset g_def head_def tail_def)
  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 (simp add: simp_eq_emptyset)
   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"
  by (simp add: Disjunctive_fun_def mono_fun_def)

theorem LinkMark_DataRefinement_a [simp]:
 "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
  apply (simp add: DgrDataRefinement2_def dgr_demonic_def LinkMark_def 
    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›

theorem LinkMark_correct:
  "Hoare_dgr (R'_a .. (R_a .. SetMarkInv)) LinkMark ((R'_a .. (R_a .. SetMarkInv)) ⊓ (- grd (step LinkMark)))"
  apply (rule_tac D = "StackMark_a" in Diagram_DataRefinement2)
  apply simp_all
  by (rule StackMark_correct)

end
end