section ‹The Single Mutator Case›

theory Gar_Coll imports Graph OG_Syntax begin

declare psubsetE [rule del]

text ‹Declaration of variables:›

record gar_coll_state =
  M :: nodes
  E :: edges
  bc :: "nat set"
  obc :: "nat set"
  Ma :: nodes
  ind :: nat
  k :: nat
  z :: bool

subsection ‹The Mutator›

text ‹The mutator first redirects an arbitrary edge ‹R› from
  arbitrary accessible node towards an arbitrary accessible node
 ‹T›. It then colors the new target ‹T› black.

  declare the arbitrarily selected node and edge as constants:›

consts R :: nat  T :: nat

text ‹\noindent The following predicate states, given a list of
  ‹m› and a list of edges ‹e›, the conditions
  which the selected edge ‹R› and node ‹T› are
 :›

definition Mut_init :: "gar_coll_state → bool" where
  "Mut_init ≡ « T ∈ Reach 🚫E ∧ R < length 🚫E ∧ T < length 🚫M ¬"

text ‹\noindent For the mutator we
  two modules, one for each action. An auxiliary variable
 ‹🚫z› is set to false if the mutator has already redirected an
  but has not yet colored the new target.›

definition Redirect_Edge :: "gar_coll_state ann_com" where
  "Redirect_Edge ≡ {🚫Mut_init ∧ 🚫z} ⟨🚫E:=🚫E[R:=(fst(🚫E!R), T)],, 🚫z:= (¬🚫z)⟩"

definition Color_Target :: "gar_coll_state ann_com" where
  "Color_Target ≡ {🚫Mut_init ∧ ¬🚫z} ⟨🚫M:=🚫M[T:=Black],, 🚫z:= (¬🚫z)⟩"

definition Mutator :: "gar_coll_state ann_com" where
  "Mutator ≡
  {🚫Mut_init ∧ 🚫z}
  WHILE True INV {🚫Mut_init ∧ 🚫z}
  DO Redirect_Edge ;; Color_Target OD"

subsubsection ‹Correctness of the mutator›

lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def

lemma Redirect_Edge:
  "⊨ Redirect_Edge pre(Color_Target)"
apply (unfold mutator_defs)
apply annhoare
apply(simp_all)
apply(force elim:Graph2)
done

lemma Color_Target:
  "⊨ Color_Target {🚫Mut_init ∧ 🚫z}"
apply (unfold mutator_defs)
apply annhoare
apply(simp_all)
done

lemma Mutator:
 "⊨ Mutator {False}"
apply(unfold Mutator_def)
apply annhoare
apply(simp_all add:Redirect_Edge Color_Target)
apply(simp add:mutator_defs)
done

subsection ‹The Collector›

text ‹\noindent A constant ‹M_init› is used to give ‹🚫Ma› a
  first value, defined as a list of nodes where only the ‹Roots› are black.›

consts  M_init :: nodes

definition Proper_M_init :: "gar_coll_state → bool" where
  "Proper_M_init ≡ « Blacks M_init=Roots ∧ length M_init=length 🚫M ¬"

definition Proper :: "gar_coll_state → bool" where
  "Proper ≡ « Proper_Roots 🚫M ∧ Proper_Edges(🚫M, 🚫E) ∧ 🚫Proper_M_init ¬"

definition Safe :: "gar_coll_state → bool" where
  "Safe ≡ « Reach 🚫E ⊆ Blacks 🚫M ¬"

lemmas collector_defs = Proper_M_init_def Proper_def Safe_def

subsubsection ‹Blackening the roots›

definition Blacken_Roots :: " gar_coll_state ann_com" where
  "Blacken_Roots ≡
  {🚫Proper}
  🚫ind:=0;;
  {🚫Proper ∧ 🚫ind=0}
  WHILE 🚫ind<length 🚫M
   INV {🚫Proper ∧ (∀i<🚫ind. i ∈ Roots ⟶ 🚫M!i=Black) ∧ 🚫ind≤length 🚫M}
  DO {🚫Proper ∧ (∀i<🚫ind. i ∈ Roots ⟶ 🚫M!i=Black) ∧ 🚫ind<length 🚫M}
   IF 🚫ind∈Roots THEN
   {🚫Proper ∧ (∀i<🚫ind. i ∈ Roots ⟶ 🚫M!i=Black) ∧ 🚫ind<length 🚫M ∧ 🚫ind∈Roots}
    🚫M:=🚫M[🚫ind:=Black] FI;;
   {🚫Proper ∧ (∀i<🚫ind+1. i ∈ Roots ⟶ 🚫M!i=Black) ∧ 🚫ind<length 🚫M}
    🚫ind:=🚫ind+1
  OD"

lemma Blacken_Roots:
 "⊨ Blacken_Roots {🚫Proper ∧ Roots⊆Blacks 🚫M}"
apply (unfold Blacken_Roots_def)
apply annhoare
apply(simp_all add:collector_defs Graph_defs)
apply safe
apply(simp_all add:nth_list_update)
  apply (erule less_SucE)
   apply simp+
 apply force
apply force
done

subsubsection ‹Propagating black›

definition PBInv :: "gar_coll_state → nat → bool" where
  "PBInv ≡ « λind. 🚫obc < Blacks 🚫M ∨ (∀i <ind. ¬BtoW (🚫E!i, 🚫M) ∨
   (¬🚫z ∧ i=R ∧ (snd(🚫E!R)) = T ∧ (∃r. ind ≤ r ∧ r < length 🚫E ∧ BtoW(🚫E!r,🚫M))))¬"

definition Propagate_Black_aux :: "gar_coll_state ann_com" where
  "Propagate_Black_aux ≡
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M}
  🚫ind:=0;;
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M ∧ 🚫ind=0}
  WHILE 🚫ind<length 🚫E
   INV {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
         ∧ 🚫PBInv 🚫ind ∧ 🚫ind≤length 🚫E}
  DO {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
       ∧ 🚫PBInv 🚫ind ∧ 🚫ind<length 🚫E}
   IF 🚫M!(fst (🚫E!🚫ind)) = Black THEN
    {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
       ∧ 🚫PBInv 🚫ind ∧ 🚫ind<length 🚫E ∧ 🚫M!fst(🚫E!🚫ind)=Black}
     🚫M:=🚫M[snd(🚫E!🚫ind):=Black];;
    {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
       ∧ 🚫PBInv (🚫ind + 1) ∧ 🚫ind<length 🚫E}
     🚫ind:=🚫ind+1
   FI
  OD"

lemma Propagate_Black_aux:
  "⊨ Propagate_Black_aux
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
    ∧ ( 🚫obc < Blacks 🚫M ∨ 🚫Safe)}"
apply (unfold Propagate_Black_aux_def  PBInv_def collector_defs)
apply annhoare
apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
      apply force
     apply force
    apply force
― ‹4 subgoals left›
apply clarify
apply(simp add:Proper_Edges_def Proper_Roots_def Graph6 Graph7 Graph8 Graph12)
apply (erule disjE)
 apply(rule disjI1)
 apply(erule Graph13)
 apply force
apply (case_tac "M x ! snd (E x ! ind x)=Black")
 apply (simp add: Graph10 BtoW_def)
 apply (rule disjI2)
 apply clarify
 apply (erule less_SucE)
  apply (erule_tac x=i in allE , erule (1) notE impE)
  apply simp
  apply clarify
  apply (drule_tac y = r in le_imp_less_or_eq)
  apply (erule disjE)
   apply (subgoal_tac "Suc (ind x)≤r")
    apply fast
   apply arith
  apply fast
 apply fast
apply(rule disjI1)
apply(erule subset_psubset_trans)
apply(erule Graph11)
apply fast
― ‹3 subgoals left›
apply force
apply force
― ‹last›
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
 apply (simp)
 apply(drule Graph1)
   apply simp
  apply clarify
  apply(erule allE, erule impE, assumption)
  apply force
 apply force
apply arith
done

subsubsection ‹Refining propagating black›

definition Auxk :: "gar_coll_state → bool" where
  "Auxk ≡ «🚫k<length 🚫M ∧ (🚫M!🚫k≠Black ∨ ¬BtoW(🚫E!🚫ind, 🚫M) ∨
          🚫obc<Blacks 🚫M ∨ (¬🚫z ∧ 🚫ind=R ∧ snd(🚫E!R)=T
          ∧ (∃r. 🚫ind<r ∧ r<length 🚫E ∧ BtoW(🚫E!r, 🚫M))))¬"

definition Propagate_Black :: " gar_coll_state ann_com" where
  "Propagate_Black ≡
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M}
  🚫ind:=0;;
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M ∧ 🚫ind=0}
  WHILE 🚫ind<length 🚫E
   INV {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
         ∧ 🚫PBInv 🚫ind ∧ 🚫ind≤length 🚫E}
  DO {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
       ∧ 🚫PBInv 🚫ind ∧ 🚫ind<length 🚫E}
   IF (🚫M!(fst (🚫E!🚫ind)))=Black THEN
    {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
      ∧ 🚫PBInv 🚫ind ∧ 🚫ind<length 🚫E ∧ (🚫M!fst(🚫E!🚫ind))=Black}
     🚫k:=(snd(🚫E!🚫ind));;
    {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
      ∧ 🚫PBInv 🚫ind ∧ 🚫ind<length 🚫E ∧ (🚫M!fst(🚫E!🚫ind))=Black
      ∧ 🚫Auxk}
     ⟨🚫M:=🚫M[🚫k:=Black],, 🚫ind:=🚫ind+1⟩
   ELSE {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
          ∧ 🚫PBInv 🚫ind ∧ 🚫ind<length 🚫E}
         ⟨IF (🚫M!(fst (🚫E!🚫ind)))≠Black THEN 🚫ind:=🚫ind+1 FI⟩
   FI
  OD"

lemma Propagate_Black:
  "⊨ Propagate_Black
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
    ∧ ( 🚫obc < Blacks 🚫M ∨ 🚫Safe)}"
apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
apply annhoare
apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
       apply force
      apply force
     apply force
― ‹5 subgoals left›
apply clarify
apply(simp add:BtoW_def Proper_Edges_def)
― ‹4 subgoals left›
apply clarify
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
apply (erule disjE)
 apply (rule disjI1)
 apply (erule psubset_subset_trans)
 apply (erule Graph9)
apply (case_tac "M x!k x=Black")
 apply (case_tac "M x ! snd (E x ! ind x)=Black")
  apply (simp add: Graph10 BtoW_def)
  apply (rule disjI2)
  apply clarify
  apply (erule less_SucE)
   apply (erule_tac x=i in allE , erule (1) notE impE)
   apply simp
   apply clarify
   apply (drule_tac y = r in le_imp_less_or_eq)
   apply (erule disjE)
    apply (subgoal_tac "Suc (ind x)≤r")
     apply fast
    apply arith
   apply fast
  apply fast
 apply (simp add: Graph10 BtoW_def)
 apply (erule disjE)
  apply (erule disjI1)
 apply clarify
 apply (erule less_SucE)
  apply force
 apply simp
 apply (subgoal_tac "Suc R≤r")
  apply fast
 apply arith
apply(rule disjI1)
apply(erule subset_psubset_trans)
apply(erule Graph11)
apply fast
― ‹2 subgoals left›
apply clarify
apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
apply (erule disjE)
 apply fast
apply clarify
apply (erule less_SucE)
 apply (erule_tac x=i in allE , erule (1) notE impE)
 apply simp
 apply clarify
 apply (drule_tac y = r in le_imp_less_or_eq)
 apply (erule disjE)
  apply (subgoal_tac "Suc (ind x)≤r")
   apply fast
  apply arith
 apply (simp add: BtoW_def)
apply (simp add: BtoW_def)
― ‹last›
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
 apply (simp)
 apply(drule Graph1)
   apply simp
  apply clarify
  apply(erule allE, erule impE, assumption)
  apply force
 apply force
apply arith
done

subsubsection ‹Counting black nodes›

definition CountInv :: "gar_coll_state → nat → bool" where
  "CountInv ≡ « λind. {i. i<ind ∧ 🚫Ma!i=Black}⊆🚫bc ¬"

definition Count :: " gar_coll_state ann_com" where
  "Count ≡
  {🚫Proper ∧ Roots⊆Blacks 🚫M
    ∧ 🚫obc⊆Blacks 🚫Ma ∧ Blacks 🚫Ma⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
    ∧ length 🚫Ma=length 🚫M ∧ (🚫obc < Blacks 🚫Ma ∨ 🚫Safe) ∧ 🚫bc={}}
  🚫ind:=0;;
  {🚫Proper ∧ Roots⊆Blacks 🚫M
    ∧ 🚫obc⊆Blacks 🚫Ma ∧ Blacks 🚫Ma⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
   ∧ length 🚫Ma=length 🚫M ∧ (🚫obc < Blacks 🚫Ma ∨ 🚫Safe) ∧ 🚫bc={}
   ∧ 🚫ind=0}
   WHILE 🚫ind<length 🚫M
     INV {🚫Proper ∧ Roots⊆Blacks 🚫M
           ∧ 🚫obc⊆Blacks 🚫Ma ∧ Blacks 🚫Ma⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
           ∧ length 🚫Ma=length 🚫M ∧ 🚫CountInv 🚫ind
           ∧ ( 🚫obc < Blacks 🚫Ma ∨ 🚫Safe) ∧ 🚫ind≤length 🚫M}
   DO {🚫Proper ∧ Roots⊆Blacks 🚫M
         ∧ 🚫obc⊆Blacks 🚫Ma ∧ Blacks 🚫Ma⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
         ∧ length 🚫Ma=length 🚫M ∧ 🚫CountInv 🚫ind
         ∧ ( 🚫obc < Blacks 🚫Ma ∨ 🚫Safe) ∧ 🚫ind<length 🚫M}
       IF 🚫M!🚫ind=Black
          THEN {🚫Proper ∧ Roots⊆Blacks 🚫M
                 ∧ 🚫obc⊆Blacks 🚫Ma ∧ Blacks 🚫Ma⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
                 ∧ length 🚫Ma=length 🚫M ∧ 🚫CountInv 🚫ind
                 ∧ ( 🚫obc < Blacks 🚫Ma ∨ 🚫Safe) ∧ 🚫ind<length 🚫M ∧ 🚫M!🚫ind=Black}
          🚫bc:=insert 🚫ind 🚫bc
       FI;;
      {🚫Proper ∧ Roots⊆Blacks 🚫M
        ∧ 🚫obc⊆Blacks 🚫Ma ∧ Blacks 🚫Ma⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
        ∧ length 🚫Ma=length 🚫M ∧ 🚫CountInv (🚫ind+1)
        ∧ ( 🚫obc < Blacks 🚫Ma ∨ 🚫Safe) ∧ 🚫ind<length 🚫M}
      🚫ind:=🚫ind+1
   OD"

lemma Count:
  "⊨ Count
  {🚫Proper ∧ Roots⊆Blacks 🚫M
   ∧ 🚫obc⊆Blacks 🚫Ma ∧ Blacks 🚫Ma⊆🚫bc ∧ 🚫bc⊆Blacks 🚫M ∧ length 🚫Ma=length 🚫M
   ∧ (🚫obc < Blacks 🚫Ma ∨ 🚫Safe)}"
apply(unfold Count_def)
apply annhoare
apply(simp_all add:CountInv_def Graph6 Graph7 Graph8 Graph12 Blacks_def collector_defs)
      apply force
     apply force
    apply force
   apply clarify
   apply simp
   apply(fast elim:less_SucE)
  apply clarify
  apply simp
  apply(fast elim:less_SucE)
 apply force
apply force
done

subsubsection ‹Appending garbage nodes to the free list›

axiomatization Append_to_free :: "nat × edges → edges"
where
  Append_to_free0: "length (Append_to_free (i, e)) = length e" and
  Append_to_free1: "Proper_Edges (m, e)
                   ==> Proper_Edges (m, Append_to_free(i, e))" and
  Append_to_free2: "i ∉ Reach e
     ==> n ∈ Reach (Append_to_free(i, e)) = ( n = i ∨ n ∈ Reach e)"

definition AppendInv :: "gar_coll_state → nat → bool" where
  "AppendInv ≡ «λind. ∀i<length 🚫M. ind≤i ⟶ i∈Reach 🚫E ⟶ 🚫M!i=Black¬"

definition Append :: "gar_coll_state ann_com" where
   "Append ≡
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫Safe}
  🚫ind:=0;;
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫Safe ∧ 🚫ind=0}
    WHILE 🚫ind<length 🚫M
      INV {🚫Proper ∧ 🚫AppendInv 🚫ind ∧ 🚫ind≤length 🚫M}
    DO {🚫Proper ∧ 🚫AppendInv 🚫ind ∧ 🚫ind<length 🚫M}
       IF 🚫M!🚫ind=Black THEN
          {🚫Proper ∧ 🚫AppendInv 🚫ind ∧ 🚫ind<length 🚫M ∧ 🚫M!🚫ind=Black}
          🚫M:=🚫M[🚫ind:=White]
       ELSE {🚫Proper ∧ 🚫AppendInv 🚫ind ∧ 🚫ind<length 🚫M ∧ 🚫ind∉Reach 🚫E}
              🚫E:=Append_to_free(🚫ind,🚫E)
       FI;;
     {🚫Proper ∧ 🚫AppendInv (🚫ind+1) ∧ 🚫ind<length 🚫M}
       🚫ind:=🚫ind+1
    OD"

lemma Append:
  "⊨ Append {🚫Proper}"
apply(unfold Append_def AppendInv_def)
apply annhoare
apply(simp_all add:collector_defs Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
       apply(force simp:Blacks_def nth_list_update)
      apply force
     apply force
    apply(force simp add:Graph_defs)
   apply force
  apply clarify
  apply simp
  apply(rule conjI)
   apply (erule Append_to_free1)
  apply clarify
  apply (drule_tac n = "i" in Append_to_free2)
  apply force
 apply force
apply force
done

subsubsection ‹Correctness of the Collector›

definition Collector :: " gar_coll_state ann_com" where
  "Collector ≡
\<lbrace>🚫Proper}
 WHILE True INV {🚫Proper}
 DO
  Blacken_Roots;;
  {🚫Proper ∧ Roots⊆Blacks 🚫M}
   🚫obc:={};;
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc={}}
   🚫bc:=Roots;;
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc={} ∧ 🚫bc=Roots}
   🚫Ma:=M_init;;
  {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc={} ∧ 🚫bc=Roots ∧ 🚫Ma=M_init}
   WHILE 🚫obc≠🚫bc
     INV {🚫Proper ∧ Roots⊆Blacks 🚫M
           ∧ 🚫obc⊆Blacks 🚫Ma ∧ Blacks 🚫Ma⊆🚫bc ∧ 🚫bc⊆Blacks 🚫M
           ∧ length 🚫Ma=length 🚫M ∧ (🚫obc < Blacks 🚫Ma ∨ 🚫Safe)}
   DO {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M}
       🚫obc:=🚫bc;;
       Propagate_Black;;
      {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M
        ∧ (🚫obc < Blacks 🚫M ∨ 🚫Safe)}
       🚫Ma:=🚫M;;
      {🚫Proper ∧ Roots⊆Blacks 🚫M ∧ 🚫obc⊆Blacks 🚫Ma
        ∧ Blacks 🚫Ma⊆Blacks 🚫M ∧ 🚫bc⊆Blacks 🚫M ∧ length 🚫Ma=length 🚫M
        ∧ ( 🚫obc < Blacks 🚫Ma ∨ 🚫Safe)}
       🚫bc:={};;
       Count
   OD;;
  Append
 OD"

lemma Collector:
  "⊨ Collector {False}"
apply(unfold Collector_def)
apply annhoare
apply(simp_all add: Blacken_Roots Propagate_Black Count Append)
apply(simp_all add:Blacken_Roots_def Propagate_Black_def Count_def Append_def collector_defs)
   apply (force simp add: Proper_Roots_def)
  apply force
 apply force
apply clarify
apply (erule disjE)
apply(simp add:psubsetI)
 apply(force dest:subset_antisym)
done

subsection ‹Interference Freedom›

lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def
                 Propagate_Black_def Count_def Append_def
lemmas Invariants = PBInv_def Auxk_def CountInv_def AppendInv_def
lemmas abbrev = collector_defs mutator_defs Invariants

lemma interfree_Blacken_Roots_Redirect_Edge:
 "interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)"
apply (unfold modules)
apply interfree_aux
apply safe
apply (simp_all add:Graph6 Graph12 abbrev)
done

lemma interfree_Redirect_Edge_Blacken_Roots:
  "interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)"
apply (unfold modules)
apply interfree_aux
apply safe
apply(simp add:abbrev)+
done

lemma interfree_Blacken_Roots_Color_Target:
  "interfree_aux (Some Blacken_Roots, {}, Some Color_Target)"
apply (unfold modules)
apply interfree_aux
apply safe
apply(simp_all add:Graph7 Graph8 nth_list_update abbrev)
done

lemma interfree_Color_Target_Blacken_Roots:
  "interfree_aux (Some Color_Target, {}, Some Blacken_Roots)"
apply (unfold modules )
apply interfree_aux
apply safe
apply(simp add:abbrev)+
done

lemma interfree_Propagate_Black_Redirect_Edge:
  "interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)"
apply (unfold modules )
apply interfree_aux
― ‹11 subgoals left›
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
 apply(erule Graph4)
   apply(simp)+
  apply (simp add:BtoW_def)
 apply (simp add:BtoW_def)
apply(rule conjI)
 apply (force simp add:BtoW_def)
apply(erule Graph4)
   apply simp+
― ‹7 subgoals left›
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
 apply(erule Graph4)
   apply(simp)+
  apply (simp add:BtoW_def)
 apply (simp add:BtoW_def)
apply(rule conjI)
 apply (force simp add:BtoW_def)
apply(erule Graph4)
   apply simp+
― ‹6 subgoals left›
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule conjE)+
apply(rule conjI)
 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
  apply(erule Graph4)
    apply(simp)+
   apply (simp add:BtoW_def)
  apply (simp add:BtoW_def)
 apply(rule conjI)
  apply (force simp add:BtoW_def)
 apply(erule Graph4)
    apply simp+
apply(simp add:BtoW_def nth_list_update)
apply force
― ‹5 subgoals left›
apply(clarify, simp add:abbrev Graph6 Graph12)
― ‹4 subgoals left›
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(rule conjI)
 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
  apply(erule Graph4)
    apply(simp)+
   apply (simp add:BtoW_def)
  apply (simp add:BtoW_def)
 apply(rule conjI)
  apply (force simp add:BtoW_def)
 apply(erule Graph4)
    apply simp+
apply(rule conjI)
 apply(simp add:nth_list_update)
 apply force
apply(rule impI, rule impI, erule disjE, erule disjI1, case_tac "R = (ind x)" ,case_tac "M x ! T = Black")
  apply(force simp add:BtoW_def)
 apply(case_tac "M x !snd (E x ! ind x)=Black")
  apply(rule disjI2)
  apply simp
  apply (erule Graph5)
  apply simp+
 apply(force simp add:BtoW_def)
apply(force simp add:BtoW_def)
― ‹3 subgoals left›
apply(clarify, simp add:abbrev Graph6 Graph12)
― ‹2 subgoals left›
apply(clarify, simp add:abbrev Graph6 Graph12)
apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
 apply clarify
 apply(erule Graph4)
   apply(simp)+
  apply (simp add:BtoW_def)
 apply (simp add:BtoW_def)
apply(rule conjI)
 apply (force simp add:BtoW_def)
apply(erule Graph4)
   apply simp+
done

lemma interfree_Redirect_Edge_Propagate_Black:
  "interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev)+
done

lemma interfree_Propagate_Black_Color_Target:
  "interfree_aux (Some Propagate_Black, {}, Some Color_Target)"
apply (unfold modules )
apply interfree_aux
― ‹11 subgoals left›
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)+
apply(erule conjE)+
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption,
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
― ‹7 subgoals left›
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply(erule conjE)+
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption,
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
― ‹6 subgoals left›
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply clarify
apply (rule conjI)
 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption,
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
apply(simp add:nth_list_update)
― ‹5 subgoals left›
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
― ‹4 subgoals left›
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply (rule conjI)
 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption,
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
apply(rule conjI)
apply(simp add:nth_list_update)
apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10,
      erule subset_psubset_trans, erule Graph11, force)
― ‹3 subgoals left›
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
― ‹2 subgoals left›
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
      case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
      erule allE, erule impE, assumption, erule impE, assumption,
      simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
― ‹3 subgoals left›
apply(simp add:abbrev)
done

lemma interfree_Color_Target_Propagate_Black:
  "interfree_aux (Some Color_Target, {}, Some Propagate_Black)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev)+
done

lemma interfree_Count_Redirect_Edge:
  "interfree_aux (Some Count, {}, Some Redirect_Edge)"
apply (unfold modules)
apply interfree_aux
― ‹9 subgoals left›
apply(simp_all add:abbrev Graph6 Graph12)
― ‹6 subgoals left›
apply(clarify, simp add:abbrev Graph6 Graph12,
      erule disjE,erule disjI1,rule disjI2,rule subset_trans, erule Graph3,force,force)+
done

lemma interfree_Redirect_Edge_Count:
  "interfree_aux (Some Redirect_Edge, {}, Some Count)"
apply (unfold modules )
apply interfree_aux
apply(clarify,simp add:abbrev)+
apply(simp add:abbrev)
done

lemma interfree_Count_Color_Target:
  "interfree_aux (Some Count, {}, Some Color_Target)"
apply (unfold modules )
apply interfree_aux
― ‹9 subgoals left›
apply(simp_all add:abbrev Graph7 Graph8 Graph12)
― ‹6 subgoals left›
apply(clarify,simp add:abbrev Graph7 Graph8 Graph12,
      erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+
― ‹2 subgoals left›
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
apply(rule conjI)
 apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
apply(simp add:nth_list_update)
― ‹1 subgoal left›
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12,
      erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
done

lemma interfree_Color_Target_Count:
  "interfree_aux (Some Color_Target, {}, Some Count)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev)+
apply(simp add:abbrev)
done

lemma interfree_Append_Redirect_Edge:
  "interfree_aux (Some Append, {}, Some Redirect_Edge)"
apply (unfold modules )
apply interfree_aux
apply( simp_all add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12)
apply(clarify, simp add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12, force dest:Graph3)+
done

lemma interfree_Redirect_Edge_Append:
  "interfree_aux (Some Redirect_Edge, {}, Some Append)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev Append_to_free0)+
apply (force simp add: Append_to_free2)
apply(clarify, simp add:abbrev Append_to_free0)+
done

lemma interfree_Append_Color_Target:
  "interfree_aux (Some Append, {}, Some Color_Target)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)+
apply(simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)
done

lemma interfree_Color_Target_Append:
  "interfree_aux (Some Color_Target, {}, Some Append)"
apply (unfold modules )
apply interfree_aux
apply(clarify, simp add:abbrev Append_to_free0)+
apply (force simp add: Append_to_free2)
apply(clarify,simp add:abbrev Append_to_free0)+
done

lemmas collector_mutator_interfree =
 interfree_Blacken_Roots_Redirect_Edge interfree_Blacken_Roots_Color_Target
 interfree_Propagate_Black_Redirect_Edge interfree_Propagate_Black_Color_Target
 interfree_Count_Redirect_Edge interfree_Count_Color_Target
 interfree_Append_Redirect_Edge interfree_Append_Color_Target
 interfree_Redirect_Edge_Blacken_Roots interfree_Color_Target_Blacken_Roots
 interfree_Redirect_Edge_Propagate_Black interfree_Color_Target_Propagate_Black
 interfree_Redirect_Edge_Count interfree_Color_Target_Count
 interfree_Redirect_Edge_Append interfree_Color_Target_Append

subsubsection ‹Interference freedom Collector-Mutator›

lemma interfree_Collector_Mutator:
 "interfree_aux (Some Collector, {}, Some Mutator)"
apply(unfold Collector_def Mutator_def)
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
apply(unfold modules collector_defs Mut_init_def)
apply(tactic  ‹TRYALL (interfree_aux_tac context)›)
― ‹32 subgoals left›
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
― ‹20 subgoals left›
apply(tactic‹TRYALL (clarify_tac context)›)
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic ‹TRYALL (eresolve_tac context [disjE])›)
apply simp_all
apply(tactic ‹TRYALL(EVERY'[resolve_tac context [disjI2],
 resolve_tac context @{thms subset_trans},
 eresolve_tac context @{thms Graph3},
 force_tac context,
 assume_tac context])›)
apply(tactic ‹TRYALL(EVERY'[resolve_tac context [disjI2],
 eresolve_tac context @{thms subset_trans},
 resolve_tac context @{thms Graph9},
 force_tac context])›)
apply(tactic ‹TRYALL(EVERY'[resolve_tac context [disjI1],
 eresolve_tac context @{thms psubset_subset_trans},
 resolve_tac context @{thms Graph9},
 force_tac context])›)
done

subsubsection ‹Interference freedom Mutator-Collector›

lemma interfree_Mutator_Collector:
 "interfree_aux (Some Mutator, {}, Some Collector)"
apply(unfold Collector_def Mutator_def)
apply interfree_aux
apply(simp_all add:collector_mutator_interfree)
apply(unfold modules collector_defs Mut_init_def)
apply(tactic  ‹TRYALL (interfree_aux_tac context)›)
― ‹64 subgoals left›
apply(simp_all add:nth_list_update Invariants Append_to_free0)+
apply(tactic‹TRYALL (clarify_tac context)›)
― ‹4 subgoals left›
apply force
apply(simp add:Append_to_free2)
apply force
apply(simp add:Append_to_free2)
done

subsubsection ‹The Garbage Collection algorithm›

text ‹In total there are 289 verification conditions.›

lemma Gar_Coll:
  "∥- {🚫Proper ∧ 🚫Mut_init ∧ 🚫z}
  COBEGIN
   Collector
  {False}
 ∥
   Mutator
  {False}
 COEND
  {False}"
apply oghoare
apply(force simp add: Mutator_def Collector_def modules)
apply(rule Collector)
apply(rule Mutator)
apply(simp add:interfree_Collector_Mutator)
apply(simp add:interfree_Mutator_Collector)
apply force
done

end