# Theory SetMark


section ‹Marking Using a Set›

theory SetMark
imports Graph DataRefinementIBP.DataRefinement
begin

text‹
We construct in this theory a diagram which computes all reachable nodes
from a given root node in a graph. The graph is defined in the theory
Graph and is given by a relation $next$ on the nodes of the graph.

The diagram has only three ordered situation
($\mathit{init} > \mathit{loop} > \mathit{final}$). The termination
variant is a pair of a situation and a natural number with the lexicographic
ordering. The idea of this ordering is that we can go from a bigger situation
to a smaller one, however if we stay in the same situation the second
component of the variant must decrease.

The idea of the algorithm is that it starts with a set $X$ containing the
root element and the root is marked. As long as $X$ is not empty, if $x\in X$
and $y$ is an unmarked sucessor of $x$ we add $y$ to $X$. If $x\in X$ has
no unmarked sucessors it is removed from $X$.
The algorithm terminates when $X$ is empty.
›

datatype I = init | loop | final

declare I.split [split]

instantiation I :: well_founded_transitive
begin

definition
less_I_def: "i < j ≡  (j = init ∧ (i = loop ∨ i = final)) ∨ (j = loop ∧ i = final)"

definition
less_eq_I_def:  "(i::I) ≤ (j::I) ≡ i = j ∨ i < j"

instance
proof
fix x y z :: I
assume "x < y" and "y < z" then  show  "x < z"
by auto
next
fix x y :: I
show  "x ≤ y ⟷ x = y ∨ x < y"
next
fix P fix a::I
show "P a" when "∀x. (∀ y. y < x ⟶ P y) ⟶ P x"
apply (insert that)
apply (case_tac "P final")
apply (case_tac "P loop")
by blast
qed (simp)

end

text‹
The set $\mathit{path}\ S \ \mathit{mrk}$ contains all reachable nodes from S along paths with
unmarked nodes.
›

lemma trascl_less: "x ≠ y ⟹ (a, x) ∈ R⇧* ⟹
((a,x) ∈ (R ∩ (-{y})×(-{y}))⇧* ∨  (y,x) ∈ R O (R ∩ (-{y})×(-{y}))⇧* )"
apply (drule_tac
b = x and a = a and r = R and
P = "λ x. (x ≠ y ⟶((a,x) ∈ (R ∩ (-{y})×(-{y}))⇧* ∨ (y,x) ∈ R O (R ∩ (-{y})×(-{y}))⇧* ))"
in rtrancl_induct)
apply (auto simp: Compl_insert)
apply (case_tac "ya = y")
apply auto
apply (rule_tac x = a and y = ya and z = z and r = "R ∩ ((UNIV - {y}) × (UNIV - {y}))" in rtrancl_trans)
apply auto
apply (case_tac "za = y")
apply auto
apply (drule_tac x = ya and y = za and z = z and r = "(R ∩ (UNIV - {y}) × (UNIV - {y}))" in rtrancl_trans)
by auto

lemma (in graph) add_set [simp]: "x ≠ y ⟹ x ∈ path S mrk ⟹ x ∈ path (insert y S) (insert y mrk)"
apply clarify
apply (drule_tac x = x and y = y and a = ya and R = "next ∩ (- mrk) × (- mrk)" in trascl_less)
apply simp_all
apply (case_tac "(ya, x) ∈ (next ∩ (- mrk) × - mrk ∩ (- {y}) × - {y})⇧*")
apply (rule_tac x = xa in exI)
apply simp_all
apply (rule_tac x = ya in exI)
apply simp
apply (case_tac "(next ∩ (- mrk) × - mrk ∩ (- {y}) × - {y}) = (next ∩ (- insert y mrk) × - insert y mrk)")
apply simp_all
apply safe
apply simp_all
apply (rule_tac x = y in exI)
apply simp
apply (rule_tac x = yaa in exI)
apply simp
apply (case_tac "(next ∩ (- mrk) × - mrk ∩ (- {y}) × - {y}) = (next ∩ (- insert y mrk) × - insert y mrk)")
apply simp_all
by auto

lemma (in graph) add_set2: "x ∈ path S mrk ⟹ x ∉ path (insert y S) (insert y mrk) ⟹ x = y"
apply (case_tac "x ≠ y")
by simp_all

lemma (in graph) del_stack [simp]: "(∀ y . (t, y) ∈ next ⟶ y ∈ mrk) ⟹ x ∉  mrk ⟹ x ∈ path S mrk ⟹ x ∈ path (S - {t}) mrk"
apply clarify
apply (rule_tac x = xa in exI)
apply (case_tac "x = y")
apply auto
apply (drule_tac a = y and b = x and R = "(next ∩ (- mrk) × - mrk)" in rtranclD)
apply safe
apply (drule_tac x = y and y = x in tranclD)
by auto

lemma (in graph) init_set [simp]: "x ∈ reach root ⟹ x ≠ root ⟹ x ∈ path {root} {root}"
apply (case_tac "root ≠ x")
apply (drule_tac a = root and x = x and y = root and R = "next" in trascl_less)
apply safe
apply (drule_tac a = root and b = x and R = "(next ∩ (UNIV - {root}) × (UNIV - {root}))" in rtranclD)
apply safe
apply (drule_tac x = root and y = x in tranclD)
by auto

lemma (in graph)  init_set2: "x ∈ reach root ⟹ x ∉ path {root} {root} ⟹ x = root"
apply (case_tac "root ≠ x")
apply (drule init_set)
by simp_all

subsection ‹Transitions›

definition (in graph)
"Q1_a ≡ [: X, mrk ↝ X', mrk'. (root::'node) = nil ∧ X' = {} ∧ mrk' = mrk :]"

definition (in graph)
"Q2_a ≡ [: X, mrk ↝ X', mrk' .
(root::'node) ≠ nil ∧ X' = {root::'node} ∧ mrk' = {root::'node} :]"

definition (in graph)
"Q3_a ≡ [: X, mrk ↝ X', mrk' .
(∃ x ∈ X . ∃ y . (x, y) ∈ next ∧ y ∉ mrk ∧ X' = X ∪ {y} ∧ mrk' = mrk ∪ {y}):]"

definition (in graph)
"Q4_a ≡ [: X, mrk ↝ X', mrk' .
(∃ x ∈ X . (∀ y . (x, y) ∈ next ⟶ y ∈ mrk) ∧ X' = X - {x} ∧ mrk' = mrk):]"

definition (in graph)
"Q5_a ≡ [: X, mrk ↝ X', mrk' . X = {} ∧ mrk = mrk' :]"

subsection ‹Invariants›

definition (in graph)
"Loop ≡ { (X, mrk) .
finite (-mrk) ∧ finite X ∧ X ⊆ mrk ∧
mrk ⊆ reach root ∧ reach root ∩ -mrk ⊆ path X mrk}"

definition
"trm ≡ λ (X, mrk) . 2 * card (-mrk) + card X"

definition
"term_eq t w = {s . t s = w}"

definition
"term_less t w = {s . t s < w}"

lemma union_term_eq [simp]:  "(⋃ w . term_eq t w) = UNIV"
by auto

lemma union_less_term_eq [simp]: "(⋃v∈{v. v < w}. term_eq t v) = term_less t w"
by auto

definition (in graph)
"Init ≡ { (X::('node set), mrk::('node set)) . finite (-mrk) ∧ mrk = {}}"

definition (in graph)
"Final ≡ { (X::('node set), mrk::('node set)) . mrk = reach root}"

definition (in graph)
"SetMarkInv i = (case i of
I.init  ⇒ Init |
I.loop  ⇒ Loop |
I.final ⇒ Final)"

definition (in graph)
"SetMarkInvFinal i = (case i of
I.final  ⇒ Final |
_  ⇒ {})"

definition  (in graph) [simp]:
"SetMarkInvTerm w i = (case i of
I.init  ⇒ Init |
I.loop  ⇒ Loop ∩ {s . trm s = w} |
I.final ⇒ Final)"

subsection ‹Diagram›

definition (in graph)
"SetMark ≡ λ (i, j) . (case (i, j) of
(I.init, I.loop)  ⇒ Q1_a ⊓ Q2_a |
(I.loop, I.loop)  ⇒ Q3_a ⊓ Q4_a |
(I.loop, I.final) ⇒ Q5_a |
_ ⇒ top)"

lemma (in graph)  SetMark_dmono [simp]:
"dmono SetMark"
apply (unfold dmono_def SetMark_def Q1_a_def Q2_a_def Q3_a_def Q4_a_def Q5_a_def)
by simp

subsection ‹Correctness of the transitions›

lemma  (in graph) init_loop_1_a[simp]: "⊨ Init {| Q1_a |} Loop"
apply (unfold hoare_demonic Init_def Q1_a_def Loop_def)
by auto

lemma  (in graph) init_loop_2_a[simp]: "⊨ Init {| Q2_a |} Loop"
apply (simp add: hoare_demonic Init_def Q2_a_def Loop_def)
apply auto
apply (rule init_set2)

lemma  (in graph) loop_loop_1_a [simp]: "⊨ (Loop ∩  {s . trm s = w}) {| Q3_a |} (Loop ∩ {s. trm s < w})"
apply (simp add: hoare_demonic Q3_a_def Loop_def trm_def)
apply safe
apply (simp_all)
apply safe
apply (rule rtrancl_into_rtrancl)
apply simp_all
apply (case_tac "card (-b) > 0")
by auto

lemma  (in graph) loop_loop_2_a[simp]: "⊨ (Loop ∩  {s . trm s = w}) {| Q4_a |} (Loop ∩ {s. trm s < w})"
apply (simp add: hoare_demonic Q4_a_def Loop_def trm_def)
apply auto
apply (case_tac "card a > 0")
by auto

lemma  (in graph) loop_final_a [simp]: "⊨ (Loop ∩ {s . trm s = w}) {| Q5_a |} Final"
apply (simp add: hoare_demonic Q5_a_def Loop_def Final_def subset_eq Int_def path_def)
by auto

lemma union_term_w[simp]:  "(⋃w. {s. t s = w}) = UNIV"
by auto

lemma union_less_term_w[simp]: "(⋃v∈{v. v < w}. {s. t s = v}) = {s . t s < w}"
by auto

lemma sup_union[simp]: "Sup (range A) i =  (⋃ w . A w i)"

lemma forall_simp [simp]: "(∀a b. ∀x∈A. (a = (t x)) ⟶ (h x) ∨ b ≠ u x) = (∀x∈ A . h x)"
by auto

lemma forall_simp2 [simp]: "(∀a b. ∀x∈A. ∀y. (a  = t x y) ⟶ (h x y) ⟶ (g x y) ∨ b ≠ u x y) = (∀x∈A. ∀y. h x y ⟶ g x y)"
by auto

subsection ‹Diagram correctness›

text‹
The termination ordering for the $\mathit{SetMark}$ diagram is the lexicographic
ordering on pairs $(i,\, n)$ where $i\in I$ and $n\in \mathit{nat}$.
›

interpretation  DiagramTermination "λ (n::nat) (i :: I) . (i, n)"
done

theorem (in graph) SetMark_correct:
"⊨ SetMarkInv {|pt SetMark|} SetMarkInvFinal"
proof (rule_tac X = "SetMarkInvTerm" in hoare_diagram3)
show "dmono SetMark" by simp
show "∀u i j. ⊨ SetMarkInvTerm u i{| SetMark (i, j) |}
DiagramTermination.SUP_L_P (λn i. (i, n)) SetMarkInvTerm (i, u) j"
by (auto simp add: SUP_L_P_def  less_pair_def less_I_def hoare_choice SetMark_def)
show "SetMarkInv ≤ Sup (range SetMarkInvTerm)"
apply (case_tac x)
apply auto
done
show "Sup (range SetMarkInvTerm) ⊓ - grd (step SetMark) ≤ SetMarkInvFinal"
apply (simp add: le_fun_def inf_fun_def SetMarkInvFinal_def)
apply safe
apply simp_all
apply (drule_tac x="I.loop" in spec)
apply (frule_tac x="I.loop" in spec)
apply (drule_tac x="I.final" in spec)
apply (simp add: Q3_a_def Q4_a_def Q5_a_def)
apply (auto)
done
qed

theorem (in graph) SetMark_correct1 [simp]:
"Hoare_dgr SetMarkInv SetMark (SetMarkInv ⊓ (- grd (step SetMark)))"
apply (rule_tac x = SetMarkInvTerm in exI)
apply (subgoal_tac "SetMarkInv = ⨆range SetMarkInvTerm")
apply simp
apply safe