# Theory Gar_Coll

Up to index of Isabelle/HOL/HoareParallel

theory Gar_Coll
imports Graph OG_Syntax
begin

    header {* \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 @{text "R"} from
    an arbitrary accessible node towards an arbitrary accessible node
    @{text "T"}.  It then colors the new target @{text "T"} black.

    We declare the arbitrarily selected node and edge as constants:*}

    consts R :: nat  T :: nat

    text {* \noindent The following predicate states, given a list of
    nodes @{text "m"} and a list of edges @{text "e"}, the conditions
    under which the selected edge @{text "R"} and node @{text "T"} are
    valid: *}

    constdefs
      Mut_init :: "gar_coll_state => bool"
      "Mut_init ≡ « T ∈ Reach ´E ∧ R < length ´E ∧ T < length ´M »"

    text {* \noindent For the mutator we
    consider two modules, one for each action.  An auxiliary variable
    @{text "´z"} is set to false if the mutator has already redirected an
    edge but has not yet colored the new target.   *}

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

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

      Mutator :: "gar_coll_state ann_com"
      "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:
      "\<turnstile> Redirect_Edge pre(Color_Target)"
    apply (unfold mutator_defs)
    apply annhoare
    apply(simp_all)
    apply(force elim:Graph2)
    done

    lemma Color_Target:
      "\<turnstile> Color_Target .{´Mut_init ∧ ´z}."
    apply (unfold mutator_defs)
    apply annhoare
    apply(simp_all)
    done

    lemma Mutator:
     "\<turnstile> Mutator .{False}."
    apply(unfold Mutator_def)
    apply annhoare
    apply(simp_all add:Redirect_Edge Color_Target)
    apply(simp add:mutator_defs Redirect_Edge_def)
    done

    subsection {* The Collector *}

    text {* \noindent A constant @{text "M_init"} is used to give @{text "´Ma"} a
    suitable first value, defined as a list of nodes where only the @{text
    "Roots"} are black. *}

    consts  M_init :: nodes

    constdefs
      Proper_M_init :: "gar_coll_state => bool"
      "Proper_M_init ≡  « Blacks M_init=Roots ∧ length M_init=length ´M »"

      Proper :: "gar_coll_state => bool"
      "Proper ≡ « Proper_Roots ´M ∧ Proper_Edges(´M, ´E) ∧ ´Proper_M_init »"

      Safe :: "gar_coll_state => bool"
      "Safe ≡ « Reach ´E ⊆ Blacks ´M »"

    lemmas collector_defs = Proper_M_init_def Proper_def Safe_def

    subsubsection {* Blackening the roots *}

    constdefs
      Blacken_Roots :: " gar_coll_state ann_com"
      "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:
     "\<turnstile> 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 *}

    constdefs
      PBInv :: "gar_coll_state => nat => bool"
      "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))))»"

    constdefs
      Propagate_Black_aux :: "gar_coll_state ann_com"
      "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:
      "\<turnstile>  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 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 (rotate_tac -1)
     apply (simp (asm_lr))
     apply(drule Graph1)
       apply simp
      apply clarify
     apply(erule allE, erule impE, assumption)
      apply force
     apply force
    apply arith
    done

    subsubsection {* Refining propagating black *}

    constdefs
      Auxk :: "gar_coll_state => bool"
      "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))))»"

    constdefs
      Propagate_Black :: " gar_coll_state ann_com"
      "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:
      "\<turnstile>  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 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
    --{* 3 subgoals left *}
    apply force
    --{* 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 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 (rotate_tac -1)
     apply (simp (asm_lr))
     apply(drule Graph1)
       apply simp
      apply clarify
     apply(erule allE, erule impE, assumption)
      apply force
     apply force
    apply arith
    done

    subsubsection {* Counting black nodes *}

    constdefs
      CountInv :: "gar_coll_state => nat => bool"
      "CountInv ≡ « λind. {i. i<ind ∧ ´Ma!i=Black}⊆´bc »"

    constdefs
      Count :: " gar_coll_state ann_com"
      "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:
      "\<turnstile> 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 *}

    consts Append_to_free :: "nat × edges => edges"

    axioms
      Append_to_free0: "length (Append_to_free (i, e)) = length e"
      Append_to_free1: "Proper_Edges (m, e)
                       ==> Proper_Edges (m, Append_to_free(i, e))"
      Append_to_free2: "i ∉ Reach e
         ==> n ∈ Reach (Append_to_free(i, e)) = ( n = i ∨ n ∈ Reach e)"

    constdefs
      AppendInv :: "gar_coll_state => nat => bool"
      "AppendInv ≡ «λind. ∀i<length ´M. ind≤i --> i∈Reach ´E --> ´M!i=Black»"

    constdefs
      Append :: " gar_coll_state ann_com"
       "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:
      "\<turnstile> 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 *}

    constdefs
      Collector :: " gar_coll_state ann_com"
      "Collector ≡
    .{´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:
      "\<turnstile> 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 mutator_defs)
    apply(tactic  {* TRYALL (interfree_aux_tac) *})
    --{* 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 *})
    apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
    apply(tactic {* TRYALL (etac disjE) *})
    apply simp_all
    apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac (thm "Graph3"),Force_tac, assume_tac]) *})
    apply(tactic {* TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac (thm "Graph9"),Force_tac]) *})
    apply(tactic {* TRYALL(EVERY'[rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),Force_tac]) *})
    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 mutator_defs)
    apply(tactic  {* TRYALL (interfree_aux_tac) *})
    --{* 64 subgoals left *}
    apply(simp_all add:nth_list_update Invariants Append_to_free0)+
    apply(tactic{* TRYALL Clarify_tac *})
    --{* 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:
      "\<parallel>- .{´Proper ∧ ´Mut_init ∧ ´z}.
      COBEGIN
       Collector
      .{False}.
     \<parallel>
       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

### The Mutator

#### Correctness of the mutator

lemmas mutator_defs:

      Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)

      Redirect_Edge == .{´Mut_init ∧ ´z}.
      ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩

      Color_Target == .{´Mut_init ∧ ¬ ´z}.
      ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩

lemmas mutator_defs:

      Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)

      Redirect_Edge == .{´Mut_init ∧ ´z}.
      ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩

      Color_Target == .{´Mut_init ∧ ¬ ´z}.
      ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩

lemma Redirect_Edge:

      \<turnstile> Redirect_Edge
         pre Color_Target

lemma Color_Target:

      \<turnstile> Color_Target
         .{´Mut_init ∧ ´z}.

lemma Mutator:

      \<turnstile> Mutator
         .{False}.

### The Collector

lemmas collector_defs:

      Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)

      Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s

      Safe == %s. Reach (E s) ⊆ Blacks (M s)

lemmas collector_defs:

      Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)

      Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s

      Safe == %s. Reach (E s) ⊆ Blacks (M s)

#### Blackening the roots

lemma Blacken_Roots:

      \<turnstile> Blacken_Roots
         .{´Proper ∧ Roots ⊆ Blacks ´M}.

#### Propagating black

lemma Propagate_Black_aux:

      \<turnstile> Propagate_Black_aux
         .{´Proper ∧
           Roots ⊆ Blacks ´M ∧
           ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ (´obc ⊂ Blacks ´M ∨ ´Safe)}.

#### Refining propagating black

lemma Propagate_Black:

      \<turnstile> Propagate_Black
         .{´Proper ∧
           Roots ⊆ Blacks ´M ∧
           ´obc ⊆ Blacks ´M ∧ ´bc ⊆ Blacks ´M ∧ (´obc ⊂ Blacks ´M ∨ ´Safe)}.

#### Counting black nodes

lemma Count:

      \<turnstile> Count
         .{´Proper ∧
           Roots ⊆ Blacks ´M ∧
           ´obc ⊆ Blacks ´Ma ∧
           Blacks ´Ma ⊆ ´bc ∧
           ´bc ⊆ Blacks ´M ∧ length ´Ma = length ´M ∧ (´obc ⊂ Blacks ´Ma ∨ ´Safe)}.

#### Appending garbage nodes to the free list

lemma Append:

      \<turnstile> Append
         .{´Proper}.

#### Correctness of the Collector

lemma Collector:

      \<turnstile> Collector
         .{False}.

### Interference Freedom

lemmas modules:

      Redirect_Edge == .{´Mut_init ∧ ´z}.
      ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩

      Color_Target == .{´Mut_init ∧ ¬ ´z}.
      ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩

      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

      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

      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

      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

lemmas modules:

      Redirect_Edge == .{´Mut_init ∧ ´z}.
      ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩

      Color_Target == .{´Mut_init ∧ ¬ ´z}.
      ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩

      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

      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

      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

      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

lemmas Invariants:

      PBInv ==
      %s ind.
         obc s ⊂ Blacks (M s) ∨
         (∀i<ind.
             ¬ BtoW (E s ! i, M s) ∨
             ¬ z s ∧
             i = R ∧
             snd (E s ! R) = T ∧
             (∃r. ind ≤ r ∧ r < length (E s) ∧ BtoW (E s ! r, M s)))

      Auxk ==
      %s. k s < length (M s) ∧
          (M s ! k s ≠ Black ∨
           ¬ BtoW (E s ! ind s, M s) ∨
           obc s ⊂ Blacks (M s) ∨
           ¬ z s ∧
           ind s = R ∧
           snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))

      CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s

      AppendInv ==
      %s ind. ∀i<length (M s). ind ≤ i --> i ∈ Reach (E s) --> M s ! i = Black

lemmas Invariants:

      PBInv ==
      %s ind.
         obc s ⊂ Blacks (M s) ∨
         (∀i<ind.
             ¬ BtoW (E s ! i, M s) ∨
             ¬ z s ∧
             i = R ∧
             snd (E s ! R) = T ∧
             (∃r. ind ≤ r ∧ r < length (E s) ∧ BtoW (E s ! r, M s)))

      Auxk ==
      %s. k s < length (M s) ∧
          (M s ! k s ≠ Black ∨
           ¬ BtoW (E s ! ind s, M s) ∨
           obc s ⊂ Blacks (M s) ∨
           ¬ z s ∧
           ind s = R ∧
           snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))

      CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s

      AppendInv ==
      %s ind. ∀i<length (M s). ind ≤ i --> i ∈ Reach (E s) --> M s ! i = Black

lemmas abbrev:

      Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)

      Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s

      Safe == %s. Reach (E s) ⊆ Blacks (M s)

      Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)

      Redirect_Edge == .{´Mut_init ∧ ´z}.
      ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩

      Color_Target == .{´Mut_init ∧ ¬ ´z}.
      ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩

      PBInv ==
      %s ind.
         obc s ⊂ Blacks (M s) ∨
         (∀i<ind.
             ¬ BtoW (E s ! i, M s) ∨
             ¬ z s ∧
             i = R ∧
             snd (E s ! R) = T ∧
             (∃r. ind ≤ r ∧ r < length (E s) ∧ BtoW (E s ! r, M s)))

      Auxk ==
      %s. k s < length (M s) ∧
          (M s ! k s ≠ Black ∨
           ¬ BtoW (E s ! ind s, M s) ∨
           obc s ⊂ Blacks (M s) ∨
           ¬ z s ∧
           ind s = R ∧
           snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))

      CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s

      AppendInv ==
      %s ind. ∀i<length (M s). ind ≤ i --> i ∈ Reach (E s) --> M s ! i = Black

lemmas abbrev:

      Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)

      Proper == %s. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s

      Safe == %s. Reach (E s) ⊆ Blacks (M s)

      Mut_init == %s. T ∈ Reach (E s) ∧ R < length (E s) ∧ T < length (M s)

      Redirect_Edge == .{´Mut_init ∧ ´z}.
      ⟨´E := ´E[R := (fst (´E ! R), T)],, ´z := (¬ ´z)⟩

      Color_Target == .{´Mut_init ∧ ¬ ´z}.
      ⟨´M := ´M[T := Black],, ´z := (¬ ´z)⟩

      PBInv ==
      %s ind.
         obc s ⊂ Blacks (M s) ∨
         (∀i<ind.
             ¬ BtoW (E s ! i, M s) ∨
             ¬ z s ∧
             i = R ∧
             snd (E s ! R) = T ∧
             (∃r. ind ≤ r ∧ r < length (E s) ∧ BtoW (E s ! r, M s)))

      Auxk ==
      %s. k s < length (M s) ∧
          (M s ! k s ≠ Black ∨
           ¬ BtoW (E s ! ind s, M s) ∨
           obc s ⊂ Blacks (M s) ∨
           ¬ z s ∧
           ind s = R ∧
           snd (E s ! R) = T ∧ (∃r>ind s. r < length (E s) ∧ BtoW (E s ! r, M s)))

      CountInv == %s ind. .{´op < ind ∧ ´(op ! (Ma s)) = Black}. ⊆ bc s

      AppendInv ==
      %s ind. ∀i<length (M s). ind ≤ i --> i ∈ Reach (E s) --> M s ! i = Black

lemma interfree_Blacken_Roots_Redirect_Edge:

      interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)

lemma interfree_Redirect_Edge_Blacken_Roots:

      interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)

lemma interfree_Blacken_Roots_Color_Target:

      interfree_aux (Some Blacken_Roots, {}, Some Color_Target)

lemma interfree_Color_Target_Blacken_Roots:

      interfree_aux (Some Color_Target, {}, Some Blacken_Roots)

lemma interfree_Propagate_Black_Redirect_Edge:

      interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)

lemma interfree_Redirect_Edge_Propagate_Black:

      interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)

lemma interfree_Propagate_Black_Color_Target:

      interfree_aux (Some Propagate_Black, {}, Some Color_Target)

lemma interfree_Color_Target_Propagate_Black:

      interfree_aux (Some Color_Target, {}, Some Propagate_Black)

lemma interfree_Count_Redirect_Edge:

      interfree_aux (Some Count, {}, Some Redirect_Edge)

lemma interfree_Redirect_Edge_Count:

      interfree_aux (Some Redirect_Edge, {}, Some Count)

lemma interfree_Count_Color_Target:

      interfree_aux (Some Count, {}, Some Color_Target)

lemma interfree_Color_Target_Count:

      interfree_aux (Some Color_Target, {}, Some Count)

lemma interfree_Append_Redirect_Edge:

      interfree_aux (Some Append, {}, Some Redirect_Edge)

lemma interfree_Redirect_Edge_Append:

      interfree_aux (Some Redirect_Edge, {}, Some Append)

lemma interfree_Append_Color_Target:

      interfree_aux (Some Append, {}, Some Color_Target)

lemma interfree_Color_Target_Append:

      interfree_aux (Some Color_Target, {}, Some Append)

lemmas collector_mutator_interfree:

      interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)

      interfree_aux (Some Blacken_Roots, {}, Some Color_Target)

      interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)

      interfree_aux (Some Propagate_Black, {}, Some Color_Target)

      interfree_aux (Some Count, {}, Some Redirect_Edge)

      interfree_aux (Some Count, {}, Some Color_Target)

      interfree_aux (Some Append, {}, Some Redirect_Edge)

      interfree_aux (Some Append, {}, Some Color_Target)

      interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)

      interfree_aux (Some Color_Target, {}, Some Blacken_Roots)

      interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)

      interfree_aux (Some Color_Target, {}, Some Propagate_Black)

      interfree_aux (Some Redirect_Edge, {}, Some Count)

      interfree_aux (Some Color_Target, {}, Some Count)

      interfree_aux (Some Redirect_Edge, {}, Some Append)

      interfree_aux (Some Color_Target, {}, Some Append)

lemmas collector_mutator_interfree:

      interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)

      interfree_aux (Some Blacken_Roots, {}, Some Color_Target)

      interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)

      interfree_aux (Some Propagate_Black, {}, Some Color_Target)

      interfree_aux (Some Count, {}, Some Redirect_Edge)

      interfree_aux (Some Count, {}, Some Color_Target)

      interfree_aux (Some Append, {}, Some Redirect_Edge)

      interfree_aux (Some Append, {}, Some Color_Target)

      interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)

      interfree_aux (Some Color_Target, {}, Some Blacken_Roots)

      interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)

      interfree_aux (Some Color_Target, {}, Some Propagate_Black)

      interfree_aux (Some Redirect_Edge, {}, Some Count)

      interfree_aux (Some Color_Target, {}, Some Count)

      interfree_aux (Some Redirect_Edge, {}, Some Append)

      interfree_aux (Some Color_Target, {}, Some Append)

#### Interference freedom Collector-Mutator

lemma interfree_Collector_Mutator:

      interfree_aux (Some Collector, {}, Some Mutator)

#### Interference freedom Mutator-Collector

lemma interfree_Mutator_Collector:

      interfree_aux (Some Mutator, {}, Some Collector)

#### The Garbage Collection algorithm

lemma Gar_Coll:

      \<parallel>- .{´Proper ∧ ´Mut_init ∧ ´z}.
         COBEGIN
         Collector
         .{False}.
         \<parallel>
         Mutator
         .{False}.
         COEND
         .{False}.