Theory SetMark (Isabelle2009-2: June 2010)


header {*  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"
    apply (simp add: less_I_def);
    by auto;
  next;
fix x y :: I
  show  "x ≤ y <-> x = y ∨ x < y";
    by (simp add: less_eq_I_def);
  next;
fix P fix a::I
  show " (∀ x. (∀ y. y < x --> P y) --> P x) ==> P a";
    apply (case_tac "P final");
    apply (case_tac "P loop");
    apply (simp_all add: less_I_def);
    by blast;
next;
qed (simp);

end

definition (in graph)
  "reach x ≡ {y . (x, y) ∈ next\<^sup>^* ∧ y ≠ nil}";

theorem (in graph) reach_nil [simp]: "reach nil = {}";
  apply (simp add: reach_def, safe);
  apply (drule rtrancl_induct);
  by auto;

theorem (in graph)  reach_next: "b ∈ reach a ==> (b, c) ∈ next ==> c ∈ reach a"
  apply (simp add: reach_def);
  by auto;

definition (in graph) 
  "path S mrk ≡ {x . (∃ s . s ∈ S ∧ (s, x) ∈ next O (next ∩ ((-mrk)×(-mrk)))\<^sup>^* )}";

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

lemma (in graph) trascl_less: "x ≠ y ==> (a, x) ∈ R\<^sup>^* ==> 
    ((a,x) ∈ (R ∩ (-{y})×(-{y}))\<^sup>^* ∨  (y,x) ∈ R O (R ∩ (-{y})×(-{y}))\<^sup>^* )";
  apply (drule_tac 
    b = x and a = a and r = R and 
    P = "λ x. (x ≠ y -->((a,x) ∈ (R ∩ (-{y})×(-{y}))\<^sup>^* ∨ (y,x) ∈ R O (R ∩ (-{y})×(-{y}))\<^sup>^* ))"
    in rtrancl_induct);
  apply auto;
  apply (case_tac "ya = y");
  apply auto;
  apply (rule_tac a = a and b = ya and c = z and r = "R ∩ ((UNIV - {y}) × (UNIV - {y}))" in rtrancl_trans);
  apply auto;
  apply (case_tac "za = y");
  apply auto;
  apply (drule_tac a = ya and b = za and c = 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 (simp add: path_def);
  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})\<^sup>^*");
  apply (rule_tac x = xa in exI);
  apply simp_all;
  apply (simp add: rel_comp_def);
  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 (simp add: rel_comp_def);
  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");
  apply (frule add_set);
  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 (simp add: path_def);
  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 (simp add: reach_def path_def);
  apply (case_tac "root ≠ x");
  apply (drule_tac a = root and x = x and y = root and R = "next" in trascl_less);
  apply simp_all;
  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 ≡ λ  (X::('node set), mrk::('node set)) . { (X'::('node set), mrk') . (root::'node) = nil ∧ X' = {} ∧ mrk' = mrk}";

definition (in graph) 
  "Q2 ≡ λ (X::('node set), mrk::('node set)) . { (X', mrk') . (root::'node) ≠ nil ∧ X' = {root::'node} ∧ mrk' = {root::'node}}";

definition (in graph) 
  "Q3 ≡ λ (X, mrk) . { (X', mrk') . 
        (∃ x ∈ X . ∃ y . (x, y) ∈ next ∧ y ∉ mrk ∧ X' = X ∪ {y} ∧ mrk' = mrk ∪ {y})}";

definition (in graph) 
  "Q4 ≡ λ (X, mrk) . { (X', mrk') .  
        (∃ x ∈ X . (∀ y . (x, y) ∈ next --> y ∈ mrk) ∧ X' = X - {x} ∧ mrk' = mrk)}"

definition (in graph) 
  "Q5 ≡ λ (X::('node set), mrk::('node set)) . { (X'::('node set), 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]:  "(\<Union> w . term_eq t w) = UNIV";
  apply (simp add: term_eq_def);
  by auto;

lemma union_less_term_eq[simp]: "(\<Union>v∈{v. v < w}. term_eq t v) = term_less t w";
  apply (simp add: term_eq_def term_less_def);
  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)";

definition (in graph) 
  "SetMark_rel ≡ λ (i, j) . (case (i, j) of
      (I.init, I.loop)  => Q1 \<squnion> Q2 |
      (I.loop, I.loop)  => Q3 \<squnion> Q4 |
      (I.loop, I.final) => Q5 |
       _ => ⊥)";
  

subsection {* Diagram *}

definition (in graph) 
  "SetMark ≡ λ (i, j) . (case (i, j) of
      (I.init, I.loop)  => (demonic Q1) \<sqinter> (demonic Q2) |
      (I.loop, I.loop)  => (demonic Q3) \<sqinter> (demonic Q4) |
      (I.loop, I.final) => demonic Q5 |
       _ => top)";

lemma (in graph) dgr_dmonic_SetMark [simp]:
  "dgr_demonic SetMark_rel = SetMark";
  by (simp add: expand_fun_eq SetMark_def dgr_demonic_def SetMark_rel_def demonic_sup_inf);

lemma (in graph)  SetMark_dmono [simp]:
  "dmono SetMark";
  apply (unfold dmono_def SetMark_def);
  by simp;

subsection {* Correctness of the transitions *}

lemma  (in graph) init_loop_1[simp]: "\<Turnstile> Init {| demonic Q1 |} Loop";
  apply (unfold hoare_demonic Init_def Q1_def Loop_def);
  by auto;

lemma  (in graph) init_loop_2[simp]: "\<Turnstile> Init {| demonic Q2 |} Loop"
  apply (simp add: hoare_demonic Init_def Q2_def Loop_def);
  apply auto;
  apply (simp_all add: reach_def);
  apply (rule init_set2);
  by (simp_all add: reach_def);


 lemma  (in graph) loop_loop_1[simp]: "\<Turnstile> (Loop ∩  {s . trm s = w}) {| demonic Q3 |} (Loop ∩ {s. trm s < w})";
  apply (simp add: hoare_demonic Q3_def Loop_def trm_def);
  apply safe;
  apply (simp_all);
  apply (simp_all add: reach_def subset_eq);
  apply safe;
  apply simp_all;
  apply (rule rtrancl_into_rtrancl);
  apply (simp_all add: Int_def);
  apply (rule add_set2);
  apply simp_all;
  apply (case_tac "card (-b) > 0");
  by auto;


 lemma  (in graph) loop_loop_2[simp]: "\<Turnstile> (Loop ∩  {s . trm s = w}) {| demonic Q4 |} (Loop ∩ {s. trm s < w})";
  apply (simp add: hoare_demonic Q4_def Loop_def trm_def);
  apply auto;
  apply (case_tac "card a > 0");
  by auto;

 lemma  (in graph) loop_final[simp]: "\<Turnstile> (Loop ∩ {s . trm s = w}) {| demonic Q5 |} Final";
  apply (simp add: hoare_demonic Q5_def Loop_def Final_def subset_eq Int_def path_def);
  by auto;


lemma union_term_w[simp]:  "(\<Union>w. {s. t s = w}) = UNIV";
  by auto;

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

lemma sup_union[simp]: "SUP A i =  (\<Union> w . A w i)";
  by (simp_all add: SUP_fun_eq);

lemma empty_pred_false[simp]: "{} a = False";
  by blast;

lemma forall_simp[simp]: "(!a b. ∀ x∈ A . (a = (t x)) --> (h x) ∨ b ≠ u x) = (∀ x∈ A . h x)";
  apply safe;
  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 )";
  apply safe;
  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:
  "\<Turnstile> SetMarkInv {|pt SetMark|} SetMarkInvFinal";
  apply (rule_tac X = "SetMarkInvTerm" in hoare_diagram3);
  apply simp;
  apply safe;
  apply (simp_all add: SetMark_def SUP_L_P_def
       less_pair_def less_I_def not_grd_dgr hoare_choice SetMarkInv_def SetMarkInvFinal_def neg_fun_pred SetMark_def);
  apply auto;
  apply (case_tac x);
  apply simp_all;
  apply (drule_tac x="I.loop" in spec);
  apply (simp add: Q1_def Q2_def);
  apply auto;
  apply (frule_tac x="I.loop" in spec);
  apply (drule_tac x="I.final" in spec);
  apply (simp add: Q3_def Q4_def Q5_def);
  by auto;

theorem (in graph) SetMark_correct1 [simp]:
  "Hoare_dgr SetMarkInv SetMark (SetMarkInv \<sqinter> (- grd (step SetMark)))";
  apply (simp add: Hoare_dgr_def);
  apply (rule_tac x = SetMarkInvTerm in exI);
  apply simp;
  apply safe;
  apply (simp_all add: SetMark_def SUP_L_P_def
       less_pair_def less_I_def not_grd_dgr hoare_choice SetMarkInv_def SetMarkInvFinal_def neg_fun_pred SetMark_def);

  apply (simp_all add: expand_fun_eq);
  apply safe;
  apply (unfold SetMarkInv_def);
  apply auto;
  apply (case_tac x);
  apply simp_all;
  apply (case_tac x);
  by simp_all;


theorem (in graph) stack_not_nil [simp]:
  "(mrk, S) ∈ Loop ==> x ∈ S ==> x ≠ nil";
  apply (simp add: Loop_def reach_def);
  by auto;

end;