Quelle  Mul_Gar_Coll.thy   Sprache: Isabelle

section ‹The Multi-Mutator Case›

theory Mul_Gar_Coll imports Graph OG_Syntax begin

text ‹The full theory takes aprox. 18 minutes.›

record mut =
  Z :: bool
  R :: nat
  T :: nat

text ‹Declaration of variables:›

record mul_gar_coll_state =
  M :: nodes
  E :: edges
  bc :: "nat set"
  obc :: "nat set"
  Ma :: nodes
  ind :: nat
  k :: nat
  q :: nat
  l :: nat
  Muts :: "mut list"

subsection ‹The Mutators›

definition Mul_mut_init :: "mul_gar_coll_state \ nat \ bool" where
  "Mul_mut_init \ \ \n. n=length \Muts \ (\iMuts!i)E
                          ∧ T (🍋Muts!i)<length 🍋M) ¬"

definition Mul_Redirect_Edge  :: "nat \ nat \ mul_gar_coll_state ann_com" where
  "Mul_Redirect_Edge j n \
  {🍋Mul_mut_init n ∧ Z (🍋Muts!j)}
  ⟨IF T(🍋Muts!j) ∈ Reach 🍋E THEN
  🍋E:= 🍋E[R (🍋Muts!j):= (fst (🍋E!R(🍋Muts!j)), T (🍋Muts!j))] FI,,
  🍋Muts:= 🍋Muts[j:= (🍋Muts!j) (Z:=False)]⟩"

definition Mul_Color_Target :: "nat \ nat \ mul_gar_coll_state ann_com" where
  "Mul_Color_Target j n \
  {🍋Mul_mut_init n ∧ ¬ Z (🍋Muts!j)}
  ⟨🍋M:=🍋M[T (🍋Muts!j):=Black],, 🍋Muts:=🍋Muts[j:= (🍋Muts!j) (Z:=True)]⟩"

definition Mul_Mutator :: "nat \ nat \ mul_gar_coll_state ann_com" where
  "Mul_Mutator j n \
  {🍋Mul_mut_init n ∧ Z (🍋Muts!j)}
  WHILE True
    INV {🍋Mul_mut_init n ∧ Z (🍋Muts!j)}
  DO Mul_Redirect_Edge j n ;;
     Mul_Color_Target j n
  OD"

lemmas mul_mutator_defs = Mul_mut_init_def Mul_Redirect_Edge_def Mul_Color_Target_def

subsubsection ‹Correctness of the proof outline of one mutator›

lemma Mul_Redirect_Edge: "0\j \ j
  ⊨ Mul_Redirect_Edge j n
     pre(Mul_Color_Target j n)"
apply (unfold mul_mutator_defs)
apply annhoare
apply(simp_all)
apply clarify
apply(simp add:nth_list_update)
done

lemma Mul_Color_Target: "0\j \ j
  ⊨  Mul_Color_Target j n
    {🍋Mul_mut_init n ∧ Z (🍋Muts!j)}"
apply (unfold mul_mutator_defs)
apply annhoare
apply(simp_all)
apply clarify
apply(simp add:nth_list_update)
done

lemma Mul_Mutator: "0\j \ j
 ⊨ Mul_Mutator j n {False}"
apply(unfold Mul_Mutator_def)
apply annhoare
apply(simp_all add:Mul_Redirect_Edge Mul_Color_Target)
apply(simp add:mul_mutator_defs Mul_Redirect_Edge_def)
done

subsubsection ‹Interference freedom between mutators›

lemma Mul_interfree_Redirect_Edge_Redirect_Edge:
  "\0\i; ij; jj\ \
  interfree_aux (Some (Mul_Redirect_Edge i n),{}, Some(Mul_Redirect_Edge j n))"
apply (unfold mul_mutator_defs)
apply interfree_aux
apply safe
apply(simp_all add: nth_list_update)
done

lemma Mul_interfree_Redirect_Edge_Color_Target:
  "\0\i; ij; jj\ \
  interfree_aux (Some(Mul_Redirect_Edge i n),{},Some(Mul_Color_Target j n))"
apply (unfold mul_mutator_defs)
apply interfree_aux
apply safe
apply(simp_all add: nth_list_update)
done

lemma Mul_interfree_Color_Target_Redirect_Edge:
  "\0\i; ij; jj\ \
  interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Redirect_Edge j n))"
apply (unfold mul_mutator_defs)
apply interfree_aux
apply safe
apply(simp_all add:nth_list_update)
done

lemma Mul_interfree_Color_Target_Color_Target:
  " \0\i; ij; jj\ \
  interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Color_Target j n))"
apply (unfold mul_mutator_defs)
apply interfree_aux
apply safe
apply(simp_all add: nth_list_update)
done

lemmas mul_mutator_interfree =
  Mul_interfree_Redirect_Edge_Redirect_Edge Mul_interfree_Redirect_Edge_Color_Target
  Mul_interfree_Color_Target_Redirect_Edge Mul_interfree_Color_Target_Color_Target

lemma Mul_interfree_Mutator_Mutator: "\i < n; j < n; i \ j\ \
  interfree_aux (Some (Mul_Mutator i n), {}, Some (Mul_Mutator j n))"
apply(unfold Mul_Mutator_def)
apply(interfree_aux)
apply(simp_all add:mul_mutator_interfree)
apply(simp_all add: mul_mutator_defs)
apply(tactic ‹TRYALL (interfree_aux_tac 🍋)›)
apply(tactic ‹ALLGOALS (clarify_tac 🍋)›)
apply (simp_all add:nth_list_update)
done

subsubsection ‹Modular Parameterized Mutators›

lemma Mul_Parameterized_Mutators: "0
 ∥- {🍋Mul_mut_init n ∧ (∀i<n. Z (🍋Muts!i))}
 COBEGIN
 SCHEME  [0≤ j< n]
  Mul_Mutator j n
 {False}
 COEND
 {False}"
apply oghoare
apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
apply(erule Mul_Mutator)
apply(simp add:Mul_interfree_Mutator_Mutator)
apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
done

subsection ‹The Collector›

definition Queue :: "mul_gar_coll_state \ nat" where
 "Queue \ \ length (filter (\i. \ Z i \ \M!(T i) \ Black) \Muts) \"

consts  M_init :: nodes

definition Proper_M_init :: "mul_gar_coll_state \ bool" where
  "Proper_M_init \ \ Blacks M_init=Roots \ length M_init=length \M \"

definition Mul_Proper :: "mul_gar_coll_state \ nat \ bool" where
  "Mul_Proper \ \ \n. Proper_Roots \M \ Proper_Edges (\M, \E) \ \Proper_M_init \ n=length \Muts \"

definition Safe :: "mul_gar_coll_state \ bool" where
  "Safe \ \ Reach \E \ Blacks \M \"

lemmas mul_collector_defs = Proper_M_init_def Mul_Proper_def Safe_def

subsubsection ‹Blackening Roots›

definition Mul_Blacken_Roots :: "nat \ mul_gar_coll_state ann_com" where
  "Mul_Blacken_Roots n \
  {🍋Mul_Proper n}
  🍋ind:=0;;
  {🍋Mul_Proper n ∧ 🍋ind=0}
  WHILE 🍋ind<length 🍋M
    INV {🍋Mul_Proper n ∧ (∀i<🍋ind. i∈Roots ⟶ 🍋M!i=Black) ∧ 🍋ind≤length 🍋M}
  DO {🍋Mul_Proper n ∧ (∀i<🍋ind. i∈Roots ⟶ 🍋M!i=Black) ∧ 🍋ind<length 🍋M}
       IF 🍋ind∈Roots THEN
     {🍋Mul_Proper n ∧ (∀i<🍋ind. i∈Roots ⟶ 🍋M!i=Black) ∧ 🍋ind<length 🍋M ∧ 🍋ind∈Roots}
       🍋M:=🍋M[🍋ind:=Black] FI;;
     {🍋Mul_Proper n ∧ (∀i<🍋ind+1. i∈Roots ⟶ 🍋M!i=Black) ∧ 🍋ind<length 🍋M}
       🍋ind:=🍋ind+1
  OD"

lemma Mul_Blacken_Roots:
  "\ Mul_Blacken_Roots n
  {🍋Mul_Proper n ∧ Roots ⊆ Blacks 🍋M}"
apply (unfold Mul_Blacken_Roots_def)
apply annhoare
apply(simp_all add:mul_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 Mul_PBInv :: "mul_gar_coll_state \ bool" where
  "Mul_PBInv \ \\Safe \ \obc\Blacks \M \ \l<\Queue
                 ∨ (∀i<🍋ind. ¬BtoW(🍋E!i,🍋M)) ∧ 🍋l≤🍋Queue¬"

definition Mul_Auxk :: "mul_gar_coll_state \ bool" where
  "Mul_Auxk \ \\l<\Queue \ \M!\k\Black \ \BtoW(\E!\ind, \M) \ \obc\Blacks \M\"

definition Mul_Propagate_Black :: "nat \ mul_gar_coll_state ann_com" where
  "Mul_Propagate_Black n \
 {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M ∧ 🍋obc⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
  ∧ (🍋Safe ∨ 🍋l≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M)}
 🍋ind:=0;;
 {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
   ∧ 🍋obc⊆Blacks 🍋M ∧ Blacks 🍋M⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
   ∧ (🍋Safe ∨ 🍋l≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M) ∧ 🍋ind=0}
 WHILE 🍋ind<length 🍋E
  INV {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
        ∧ 🍋obc⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
        ∧ 🍋Mul_PBInv ∧ 🍋ind≤length 🍋E}
 DO {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
     ∧ 🍋obc⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
     ∧ 🍋Mul_PBInv ∧ 🍋ind<length 🍋E}
   IF 🍋M!(fst (🍋E!🍋ind))=Black THEN
   {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
     ∧ 🍋obc⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
     ∧ 🍋Mul_PBInv ∧ (🍋M!fst(🍋E!🍋ind))=Black ∧ 🍋ind<length 🍋E}
    🍋k:=snd(🍋E!🍋ind);;
   {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
     ∧ 🍋obc⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
     ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋M ∨ 🍋l<🍋Queue ∨ (∀i<🍋ind. ¬BtoW(🍋E!i,🍋M))
        ∧ 🍋l≤🍋Queue ∧ 🍋Mul_Auxk ) ∧ 🍋k<length 🍋M ∧ 🍋M!fst(🍋E!🍋ind)=Black
     ∧ 🍋ind<length 🍋E}
   ⟨🍋M:=🍋M[🍋k:=Black],,🍋ind:=🍋ind+1⟩
   ELSE {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
         ∧ 🍋obc⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
         ∧ 🍋Mul_PBInv ∧ 🍋ind<length 🍋E}
         ⟨IF 🍋M!(fst (🍋E!🍋ind))≠Black THEN 🍋ind:=🍋ind+1 FI⟩ FI
 OD"

lemma Mul_Propagate_Black:
  "\ Mul_Propagate_Black n
   {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M ∧ 🍋obc⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
     ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋M ∨ 🍋l<🍋Queue ∧ (🍋l≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))}"
apply(unfold Mul_Propagate_Black_def)
apply annhoare
apply(simp_all add:Mul_PBInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
🍋 ‹8 subgoals left›
apply force
apply force
apply force
apply(force simp add:BtoW_def Graph_defs)
🍋 ‹4 subgoals left›
apply clarify
apply(simp add: mul_collector_defs Graph12 Graph6 Graph7 Graph8)
apply(disjE_tac)
 apply(simp_all add:Graph12 Graph13)
 apply(case_tac "M x! k x=Black")
  apply(simp add: Graph10)
 apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
apply(case_tac "M x! k x=Black")
 apply(simp add: Graph10 BtoW_def)
 apply(rule disjI2, clarify, erule less_SucE, force)
 apply(case_tac "M x!snd(E x! ind x)=Black")
  apply(force)
 apply(force)
apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
🍋 ‹2 subgoals left›
apply clarify
apply(conjI_tac)
apply(disjE_tac)
 apply (simp_all)
apply clarify
apply(erule less_SucE)
 apply force
apply (simp add:BtoW_def)
🍋 ‹1 subgoal left›
apply clarify
apply simp
apply(disjE_tac)
apply (simp_all)
apply(rule disjI1 , rule Graph1)
 apply simp_all
done

subsubsection ‹Counting Black Nodes›

definition Mul_CountInv :: "mul_gar_coll_state \ nat \ bool" where
  "Mul_CountInv \ \ \ind. {i. i \Ma!i=Black}\\bc \"

definition Mul_Count :: "nat \ mul_gar_coll_state ann_com" where
  "Mul_Count n \
  {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
    ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
    ∧ length 🍋Ma=length 🍋M
    ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M) )
    ∧ 🍋q<n+1 ∧ 🍋bc={}}
  🍋ind:=0;;
  {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
    ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
    ∧ length 🍋Ma=length 🍋M
    ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M) )
    ∧ 🍋q<n+1 ∧ 🍋bc={} ∧ 🍋ind=0}
  WHILE 🍋ind<length 🍋M
     INV {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
          ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
          ∧ length 🍋Ma=length 🍋M ∧ 🍋Mul_CountInv 🍋ind
          ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))
          ∧ 🍋q<n+1 ∧ 🍋ind≤length 🍋M}
  DO {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
       ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
       ∧ length 🍋Ma=length 🍋M ∧ 🍋Mul_CountInv 🍋ind
       ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))
       ∧ 🍋q<n+1 ∧ 🍋ind<length 🍋M}
     IF 🍋M!🍋ind=Black
     THEN {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
            ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
            ∧ length 🍋Ma=length 🍋M ∧ 🍋Mul_CountInv 🍋ind
            ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))
            ∧ 🍋q<n+1 ∧ 🍋ind<length 🍋M ∧ 🍋M!🍋ind=Black}
          🍋bc:=insert 🍋ind 🍋bc
     FI;;
  {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
    ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
    ∧ length 🍋Ma=length 🍋M ∧ 🍋Mul_CountInv (🍋ind+1)
    ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))
    ∧ 🍋q<n+1 ∧ 🍋ind<length 🍋M}
  🍋ind:=🍋ind+1
  OD"

lemma Mul_Count:
  "\ Mul_Count n
  {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
    ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
    ∧ length 🍋Ma=length 🍋M ∧ Blacks 🍋Ma⊆🍋bc
    ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))
    ∧ 🍋q<n+1}"
apply (unfold Mul_Count_def)
apply annhoare
apply(simp_all add:Mul_CountInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
🍋 ‹7 subgoals left›
apply force
apply force
apply force
🍋 ‹4 subgoals left›
apply clarify
apply(conjI_tac)
apply(disjE_tac)
 apply simp_all
apply(simp add:Blacks_def)
apply clarify
apply(erule less_SucE)
 back
 apply force
apply force
🍋 ‹3 subgoals left›
apply clarify
apply(conjI_tac)
apply(disjE_tac)
 apply simp_all
apply clarify
apply(erule less_SucE)
 back
 apply force
apply simp
apply(rotate_tac -1)
apply (force simp add:Blacks_def)
🍋 ‹2 subgoals left›
apply force
🍋 ‹1 subgoal left›
apply clarify
apply(drule_tac x = "ind x" in le_imp_less_or_eq)
apply (simp_all add:Blacks_def)
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 Mul_AppendInv :: "mul_gar_coll_state \ nat \ bool" where
  "Mul_AppendInv \ \ \ind. (\i. ind\i \ iM \ i\Reach \E \ \M!i=Black)\"

definition Mul_Append :: "nat \ mul_gar_coll_state ann_com" where
  "Mul_Append n \
  {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M ∧ 🍋Safe}
  🍋ind:=0;;
  {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M ∧ 🍋Safe ∧ 🍋ind=0}
  WHILE 🍋ind<length 🍋M
    INV {🍋Mul_Proper n ∧ 🍋Mul_AppendInv 🍋ind ∧ 🍋ind≤length 🍋M}
  DO {🍋Mul_Proper n ∧ 🍋Mul_AppendInv 🍋ind ∧ 🍋ind<length 🍋M}
      IF 🍋M!🍋ind=Black THEN
     {🍋Mul_Proper n ∧ 🍋Mul_AppendInv 🍋ind ∧ 🍋ind<length 🍋M ∧ 🍋M!🍋ind=Black}
      🍋M:=🍋M[🍋ind:=White]
      ELSE
     {🍋Mul_Proper n ∧ 🍋Mul_AppendInv 🍋ind ∧ 🍋ind<length 🍋M ∧ 🍋ind∉Reach 🍋E}
      🍋E:=Append_to_free(🍋ind,🍋E)
      FI;;
  {🍋Mul_Proper n ∧ 🍋Mul_AppendInv (🍋ind+1) ∧ 🍋ind<length 🍋M}
   🍋ind:=🍋ind+1
  OD"

lemma Mul_Append:
  "\ Mul_Append n
     {🍋Mul_Proper n}"
apply(unfold Mul_Append_def)
apply annhoare
apply(simp_all add: mul_collector_defs Mul_AppendInv_def
      Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(force simp add:Blacks_def)
apply(force simp add:Blacks_def)
apply(force simp add:Blacks_def)
apply(force simp add:Graph_defs)
apply force
apply(force simp add:Append_to_free1 Append_to_free2)
apply force
apply force
done

subsubsection ‹Collector›

definition Mul_Collector :: "nat \ mul_gar_coll_state ann_com" where
  "Mul_Collector n \
{🍋Mul_Proper n}
WHILE True INV {🍋Mul_Proper n}
DO
Mul_Blacken_Roots n ;;
{🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M}
 🍋obc:={};;
{🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M ∧ 🍋obc={}}
 🍋bc:=Roots;;
{🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M ∧ 🍋obc={} ∧ 🍋bc=Roots}
 🍋l:=0;;
{🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M ∧ 🍋obc={} ∧ 🍋bc=Roots ∧ 🍋l=0}
 WHILE 🍋l<n+1
   INV {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M ∧
         (🍋Safe ∨ (🍋l≤🍋Queue ∨ 🍋bc⊂Blacks 🍋M) ∧ 🍋l<n+1)}
 DO {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
      ∧ (🍋Safe ∨ 🍋l≤🍋Queue ∨ 🍋bc⊂Blacks 🍋M)}
    🍋obc:=🍋bc;;
    Mul_Propagate_Black n;;
    {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
      ∧ 🍋obc⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
      ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋M ∨ 🍋l<🍋Queue
      ∧ (🍋l≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))}
    🍋bc:={};;
    {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
      ∧ 🍋obc⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
      ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋M ∨ 🍋l<🍋Queue
      ∧ (🍋l≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M)) ∧ 🍋bc={}}
       ⟨ 🍋Ma:=🍋M,, 🍋q:=🍋Queue ⟩;;
    Mul_Count n;;
    {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
      ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
      ∧ length 🍋Ma=length 🍋M ∧ Blacks 🍋Ma⊆🍋bc
      ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))
      ∧ 🍋q<n+1}
    IF 🍋obc=🍋bc THEN
    {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
      ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
      ∧ length 🍋Ma=length 🍋M ∧ Blacks 🍋Ma⊆🍋bc
      ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))
      ∧ 🍋q<n+1 ∧ 🍋obc=🍋bc}
    🍋l:=🍋l+1
    ELSE {🍋Mul_Proper n ∧ Roots⊆Blacks 🍋M
          ∧ 🍋obc⊆Blacks 🍋Ma ∧ Blacks 🍋Ma⊆Blacks 🍋M ∧ 🍋bc⊆Blacks 🍋M
          ∧ length 🍋Ma=length 🍋M ∧ Blacks 🍋Ma⊆🍋bc
          ∧ (🍋Safe ∨ 🍋obc⊂Blacks 🍋Ma ∨ 🍋l<🍋q ∧ (🍋q≤🍋Queue ∨ 🍋obc⊂Blacks 🍋M))
          ∧ 🍋q<n+1 ∧ 🍋obc≠🍋bc}
        🍋l:=0 FI
 OD;;
 Mul_Append n
OD"

lemmas mul_modules = Mul_Redirect_Edge_def Mul_Color_Target_def
 Mul_Blacken_Roots_def Mul_Propagate_Black_def
 Mul_Count_def Mul_Append_def

lemma Mul_Collector:
  "\ Mul_Collector n
  {False}"
apply(unfold Mul_Collector_def)
apply annhoare
apply(simp_all only:pre.simps Mul_Blacken_Roots
       Mul_Propagate_Black Mul_Count Mul_Append)
apply(simp_all add:mul_modules)
apply(simp_all add:mul_collector_defs Queue_def)
apply force
apply force
apply force
apply (force simp add: less_Suc_eq_le)
apply force
apply (force dest:subset_antisym)
apply force
apply force
apply force
done

subsection ‹Interference Freedom›

lemma le_length_filter_update[rule_format]:
 "\i. (\P (list!i) \ P j) \ i
 ⟶ length(filter P list) ≤ length(filter P (list[i:=j]))"
apply(induct_tac "list")
 apply(simp)
apply(clarify)
apply(case_tac i)
 apply(simp)
apply(simp)
done

lemma less_length_filter_update [rule_format]:
 "\i. P j \ \(P (list!i)) \ i
 ⟶ length(filter P list) < length(filter P (list[i:=j]))"
apply(induct_tac "list")
 apply(simp)
apply(clarify)
apply(case_tac i)
 apply(simp)
apply(simp)
done

lemma Mul_interfree_Blacken_Roots_Redirect_Edge: "\0\j; j \
  interfree_aux (Some(Mul_Blacken_Roots n),{},Some(Mul_Redirect_Edge j n))"
apply (unfold mul_modules)
apply interfree_aux
apply safe
apply(simp_all add:Graph6 Graph9 Graph12 nth_list_update mul_mutator_defs mul_collector_defs)
done

lemma Mul_interfree_Redirect_Edge_Blacken_Roots: "\0\j; j\
  interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Blacken_Roots n))"
apply (unfold mul_modules)
apply interfree_aux
apply safe
apply(simp_all add:mul_mutator_defs nth_list_update)
done

lemma Mul_interfree_Blacken_Roots_Color_Target: "\0\j; j\
  interfree_aux (Some(Mul_Blacken_Roots n),{},Some (Mul_Color_Target j n ))"
apply (unfold mul_modules)
apply interfree_aux
apply safe
apply(simp_all add:mul_mutator_defs mul_collector_defs nth_list_update Graph7 Graph8 Graph9 Graph12)
done

lemma Mul_interfree_Color_Target_Blacken_Roots: "\0\j; j\
  interfree_aux (Some(Mul_Color_Target j n ),{},Some (Mul_Blacken_Roots n ))"
apply (unfold mul_modules)
apply interfree_aux
apply safe
apply(simp_all add:mul_mutator_defs nth_list_update)
done

lemma Mul_interfree_Propagate_Black_Redirect_Edge: "\0\j; j\
  interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Redirect_Edge j n ))"
apply (unfold mul_modules)
apply interfree_aux
apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_PBInv_def nth_list_update Graph6)
🍋 ‹7 subgoals left›
apply clarify
apply(disjE_tac)
  apply(simp_all add:Graph6)
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply(rule conjI)
 apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
🍋 ‹6 subgoals left›
apply clarify
apply(disjE_tac)
  apply(simp_all add:Graph6)
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply(rule conjI)
 apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
🍋 ‹5 subgoals left›
apply clarify
apply(disjE_tac)
  apply(simp_all add:Graph6)
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply(rule conjI)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(erule conjE)
apply(case_tac "M x!(T (Muts x!j))=Black")
 apply(rule conjI)
  apply(rule impI,(rule disjI2)+,rule conjI)
   apply clarify
   apply(case_tac "R (Muts x! j)=i")
    apply (force simp add: nth_list_update BtoW_def)
   apply (force simp add: nth_list_update)
  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule impI,(rule disjI2)+, erule le_trans)
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule conjI)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
🍋 ‹4 subgoals left›
apply clarify
apply(disjE_tac)
  apply(simp_all add:Graph6)
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply(rule conjI)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(erule conjE)
apply(case_tac "M x!(T (Muts x!j))=Black")
 apply(rule conjI)
  apply(rule impI,(rule disjI2)+,rule conjI)
   apply clarify
   apply(case_tac "R (Muts x! j)=i")
    apply (force simp add: nth_list_update BtoW_def)
   apply (force simp add: nth_list_update)
  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule impI,(rule disjI2)+, erule le_trans)
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule conjI)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
🍋 ‹3 subgoals left›
apply clarify
apply(disjE_tac)
  apply(simp_all add:Graph6)
  apply (rule impI)
   apply(rule conjI)
    apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   apply(case_tac "R (Muts x ! j)= ind x")
    apply(simp add:nth_list_update)
   apply(simp add:nth_list_update)
  apply(case_tac "R (Muts x ! j)= ind x")
   apply(simp add:nth_list_update)
  apply(simp add:nth_list_update)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule conjI)
   apply(rule impI)
   apply(rule conjI)
    apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   apply(case_tac "R (Muts x ! j)= ind x")
    apply(simp add:nth_list_update)
   apply(simp add:nth_list_update)
  apply(rule impI)
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule conjI)
  apply(rule impI)
   apply(rule conjI)
    apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   apply(case_tac "R (Muts x ! j)= ind x")
    apply(simp add:nth_list_update)
   apply(simp add:nth_list_update)
  apply(rule impI)
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(erule conjE)
 apply(rule conjI)
  apply(case_tac "M x!(T (Muts x!j))=Black")
   apply(rule impI,rule conjI,(rule disjI2)+,rule conjI)
    apply clarify
    apply(case_tac "R (Muts x! j)=i")
     apply (force simp add: nth_list_update BtoW_def)
    apply (force simp add: nth_list_update)
   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
  apply(case_tac "R (Muts x ! j)= ind x")
   apply(simp add:nth_list_update)
  apply(simp add:nth_list_update)
 apply(rule impI,rule conjI)
  apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
  apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
 apply(case_tac "R (Muts x! j)=ind x")
  apply (force simp add: nth_list_update)
 apply (force simp add: nth_list_update)
apply(rule impI, (rule disjI2)+, erule le_trans)
apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
🍋 ‹2 subgoals left›
apply clarify
apply(rule conjI)
 apply(disjE_tac)
  apply(simp_all add:Mul_Auxk_def Graph6)
  apply (rule impI)
   apply(rule conjI)
    apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   apply(case_tac "R (Muts x ! j)= ind x")
    apply(simp add:nth_list_update)
   apply(simp add:nth_list_update)
  apply(case_tac "R (Muts x ! j)= ind x")
   apply(simp add:nth_list_update)
  apply(simp add:nth_list_update)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule impI)
  apply(rule conjI)
   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
  apply(case_tac "R (Muts x ! j)= ind x")
   apply(simp add:nth_list_update)
  apply(simp add:nth_list_update)
 apply(rule impI)
 apply(rule conjI)
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(case_tac "R (Muts x ! j)= ind x")
  apply(simp add:nth_list_update)
 apply(simp add:nth_list_update)
apply(rule impI)
apply(rule conjI)
 apply(erule conjE)+
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply((rule disjI2)+,rule conjI)
   apply clarify
   apply(case_tac "R (Muts x! j)=i")
    apply (force simp add: nth_list_update BtoW_def)
   apply (force simp add: nth_list_update)
  apply(rule conjI)
   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
  apply(rule impI)
  apply(case_tac "R (Muts x ! j)= ind x")
   apply(simp add:nth_list_update BtoW_def)
  apply (simp  add:nth_list_update)
  apply(rule impI)
  apply simp
  apply(disjE_tac)
   apply(rule disjI1, erule less_le_trans)
   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
  apply force
 apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
 apply(case_tac "R (Muts x ! j)= ind x")
  apply(simp add:nth_list_update)
 apply(simp add:nth_list_update)
apply(disjE_tac)
apply simp_all
apply(conjI_tac)
 apply(rule impI)
 apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(erule conjE)+
apply(rule impI,(rule disjI2)+,rule conjI)
 apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule impI)+
apply simp
apply(disjE_tac)
 apply(rule disjI1, erule less_le_trans)
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply force
🍋 ‹1 subgoal left›
apply clarify
apply(disjE_tac)
  apply(simp_all add:Graph6)
 apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply(rule conjI)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(erule conjE)
apply(case_tac "M x!(T (Muts x!j))=Black")
 apply(rule conjI)
  apply(rule impI,(rule disjI2)+,rule conjI)
   apply clarify
   apply(case_tac "R (Muts x! j)=i")
    apply (force simp add: nth_list_update BtoW_def)
   apply (force simp add: nth_list_update)
  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule impI,(rule disjI2)+, erule le_trans)
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule conjI)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
done

lemma Mul_interfree_Redirect_Edge_Propagate_Black: "\0\j; j\
  interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Propagate_Black n))"
apply (unfold mul_modules)
apply interfree_aux
apply safe
apply(simp_all add:mul_mutator_defs nth_list_update)
done

lemma Mul_interfree_Propagate_Black_Color_Target: "\0\j; j\
  interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Color_Target j n ))"
apply (unfold mul_modules)
apply interfree_aux
apply(simp_all add: mul_collector_defs mul_mutator_defs)
🍋 ‹7 subgoals left›
apply clarify
apply (simp add:Graph7 Graph8 Graph12)
apply(disjE_tac)
  apply(simp add:Graph7 Graph8 Graph12)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule disjI2,rule disjI1, erule le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp)
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
🍋 ‹6 subgoals left›
apply clarify
apply (simp add:Graph7 Graph8 Graph12)
apply(disjE_tac)
  apply(simp add:Graph7 Graph8 Graph12)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule disjI2,rule disjI1, erule le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp)
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
🍋 ‹5 subgoals left›
apply clarify
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
apply(disjE_tac)
   apply(simp add:Graph7 Graph8 Graph12)
  apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
apply(erule conjE)
apply(case_tac "M x!(T (Muts x!j))=Black")
 apply((rule disjI2)+)
 apply (rule conjI)
  apply(simp add:Graph10)
 apply(erule le_trans)
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
🍋 ‹4 subgoals left›
apply clarify
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
apply(disjE_tac)
   apply(simp add:Graph7 Graph8 Graph12)
  apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
apply(erule conjE)
apply(case_tac "M x!(T (Muts x!j))=Black")
 apply((rule disjI2)+)
 apply (rule conjI)
  apply(simp add:Graph10)
 apply(erule le_trans)
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
🍋 ‹3 subgoals left›
apply clarify
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
apply(case_tac "M x!(T (Muts x!j))=Black")
 apply(simp add:Graph10)
 apply(disjE_tac)
  apply simp_all
  apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply(erule conjE)
 apply((rule disjI2)+,erule le_trans)
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
apply(rule conjI)
 apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11)
apply (force simp add:nth_list_update)
🍋 ‹2 subgoals left›
apply clarify
apply(simp add:Mul_Auxk_def Graph7 Graph8 Graph12)
apply(case_tac "M x!(T (Muts x!j))=Black")
 apply(simp add:Graph10)
 apply(disjE_tac)
  apply simp_all
  apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply(erule conjE)+
 apply((rule disjI2)+,rule conjI, erule le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply((rule impI)+)
 apply simp
 apply(erule disjE)
  apply(rule disjI1, erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply force
apply(rule conjI)
 apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11)
apply (force simp add:nth_list_update)
🍋 ‹1 subgoal left›
apply clarify
apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
apply(case_tac "M x!(T (Muts x!j))=Black")
 apply(simp add:Graph10)
 apply(disjE_tac)
  apply simp_all
  apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply(erule conjE)
 apply((rule disjI2)+,erule le_trans)
 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11)
done

lemma Mul_interfree_Color_Target_Propagate_Black: "\0\j; j\
  interfree_aux (Some(Mul_Color_Target j n),{},Some(Mul_Propagate_Black n ))"
apply (unfold mul_modules)
apply interfree_aux
apply safe
apply(simp_all add:mul_mutator_defs nth_list_update)
done

lemma Mul_interfree_Count_Redirect_Edge: "\0\j; j\
  interfree_aux (Some(Mul_Count n ),{},Some(Mul_Redirect_Edge j n))"
apply (unfold mul_modules)
apply interfree_aux
🍋 ‹9 subgoals left›
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def Graph6)
apply clarify
apply disjE_tac
   apply(simp add:Graph6)
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
 apply(simp add:Graph6)
apply clarify
apply disjE_tac
 apply(simp add:Graph6)
 apply(rule conjI)
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(simp add:Graph6)
🍋 ‹8 subgoals left›
apply(simp add:mul_mutator_defs nth_list_update)
🍋 ‹7 subgoals left›
apply(simp add:mul_mutator_defs mul_collector_defs)
apply clarify
apply disjE_tac
   apply(simp add:Graph6)
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
 apply(simp add:Graph6)
apply clarify
apply disjE_tac
 apply(simp add:Graph6)
 apply(rule conjI)
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(simp add:Graph6)
🍋 ‹6 subgoals left›
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
apply clarify
apply disjE_tac
   apply(simp add:Graph6 Queue_def)
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
 apply(simp add:Graph6)
apply clarify
apply disjE_tac
 apply(simp add:Graph6)
 apply(rule conjI)
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(simp add:Graph6)
🍋 ‹5 subgoals left›
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
apply clarify
apply disjE_tac
   apply(simp add:Graph6)
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
 apply(simp add:Graph6)
apply clarify
apply disjE_tac
 apply(simp add:Graph6)
 apply(rule conjI)
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(simp add:Graph6)
🍋 ‹4 subgoals left›
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
apply clarify
apply disjE_tac
   apply(simp add:Graph6)
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
 apply(simp add:Graph6)
apply clarify
apply disjE_tac
 apply(simp add:Graph6)
 apply(rule conjI)
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(simp add:Graph6)
🍋 ‹3 subgoals left›
apply(simp add:mul_mutator_defs nth_list_update)
🍋 ‹2 subgoals left›
apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
apply clarify
apply disjE_tac
   apply(simp add:Graph6)
  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
 apply(simp add:Graph6)
apply clarify
apply disjE_tac
 apply(simp add:Graph6)
 apply(rule conjI)
  apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
 apply(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(simp add:Graph6)
🍋 ‹1 subgoal left›
apply(simp add:mul_mutator_defs nth_list_update)
done

lemma Mul_interfree_Redirect_Edge_Count: "\0\j; j\
  interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Count n ))"
apply (unfold mul_modules)
apply interfree_aux
apply safe
apply(simp_all add:mul_mutator_defs nth_list_update)
done

lemma Mul_interfree_Count_Color_Target: "\0\j; j\
  interfree_aux (Some(Mul_Count n ),{},Some(Mul_Color_Target j n))"
apply (unfold mul_modules)
apply interfree_aux
apply(simp_all add:mul_collector_defs mul_mutator_defs Mul_CountInv_def)
🍋 ‹6 subgoals left›
apply clarify
apply disjE_tac
  apply (simp add: Graph7 Graph8 Graph12)
 apply (simp add: Graph7 Graph8 Graph12)
apply clarify
apply disjE_tac
 apply (simp add: Graph7 Graph8 Graph12)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
apply (simp add: Graph7 Graph8 Graph12)
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
🍋 ‹5 subgoals left›
apply clarify
apply disjE_tac
  apply (simp add: Graph7 Graph8 Graph12)
 apply (simp add: Graph7 Graph8 Graph12)
apply clarify
apply disjE_tac
 apply (simp add: Graph7 Graph8 Graph12)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
apply (simp add: Graph7 Graph8 Graph12)
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
🍋 ‹4 subgoals left›
apply clarify
apply disjE_tac
  apply (simp add: Graph7 Graph8 Graph12)
 apply (simp add: Graph7 Graph8 Graph12)
apply clarify
apply disjE_tac
 apply (simp add: Graph7 Graph8 Graph12)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
apply (simp add: Graph7 Graph8 Graph12)
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
🍋 ‹3 subgoals left›
apply clarify
apply disjE_tac
  apply (simp add: Graph7 Graph8 Graph12)
 apply (simp add: Graph7 Graph8 Graph12)
apply clarify
apply disjE_tac
 apply (simp add: Graph7 Graph8 Graph12)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
apply (simp add: Graph7 Graph8 Graph12)
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
🍋 ‹2 subgoals left›
apply clarify
apply disjE_tac
  apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
 apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
apply clarify
apply disjE_tac
 apply (simp add: Graph7 Graph8 Graph12)
 apply(rule conjI)
  apply(case_tac "M x!(T (Muts x!j))=Black")
   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
 apply (simp add: nth_list_update)
apply (simp add: Graph7 Graph8 Graph12)
apply(rule conjI)
 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
apply (simp add: nth_list_update)
🍋 ‹1 subgoal left›
apply clarify
apply disjE_tac
  apply (simp add: Graph7 Graph8 Graph12)
 apply (simp add: Graph7 Graph8 Graph12)
apply clarify
apply disjE_tac
 apply (simp add: Graph7 Graph8 Graph12)
 apply(case_tac "M x!(T (Muts x!j))=Black")
  apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
 apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
apply (simp add: Graph7 Graph8 Graph12)
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
done

lemma Mul_interfree_Color_Target_Count: "\0\j; j\
  interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Count n ))"
apply (unfold mul_modules)
apply interfree_aux
apply safe
apply(simp_all add:mul_mutator_defs nth_list_update)
done

lemma Mul_interfree_Append_Redirect_Edge: "\0\j; j\
  interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
apply (unfold mul_modules)
apply interfree_aux
apply(tactic ‹ALLGOALS (clarify_tac 🍋)›)
apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
apply(erule_tac x=j in allE, force dest:Graph3)+
done

lemma Mul_interfree_Redirect_Edge_Append: "\0\j; j\
  interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
apply(tactic ‹ALLGOALS (clarify_tac 🍋)›)
apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def  mul_mutator_defs nth_list_update)
done

lemma Mul_interfree_Append_Color_Target: "\0\j; j\
  interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
apply (unfold mul_modules)
apply interfree_aux
apply(tactic ‹ALLGOALS (clarify_tac 🍋)›)
apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1
              Graph12 nth_list_update)
done

lemma Mul_interfree_Color_Target_Append: "\0\j; j\
  interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
apply(tactic ‹ALLGOALS (clarify_tac 🍋)›)
apply(simp_all add: mul_mutator_defs nth_list_update)
apply(simp add:Mul_AppendInv_def Append_to_free0)
done

subsubsection ‹Interference freedom Collector-Mutator›

lemmas mul_collector_mutator_interfree =
 Mul_interfree_Blacken_Roots_Redirect_Edge Mul_interfree_Blacken_Roots_Color_Target
 Mul_interfree_Propagate_Black_Redirect_Edge Mul_interfree_Propagate_Black_Color_Target
 Mul_interfree_Count_Redirect_Edge Mul_interfree_Count_Color_Target
 Mul_interfree_Append_Redirect_Edge Mul_interfree_Append_Color_Target
 Mul_interfree_Redirect_Edge_Blacken_Roots Mul_interfree_Color_Target_Blacken_Roots
 Mul_interfree_Redirect_Edge_Propagate_Black Mul_interfree_Color_Target_Propagate_Black
 Mul_interfree_Redirect_Edge_Count Mul_interfree_Color_Target_Count
 Mul_interfree_Redirect_Edge_Append Mul_interfree_Color_Target_Append

lemma Mul_interfree_Collector_Mutator: "j
  interfree_aux (Some (Mul_Collector n), {}, Some (Mul_Mutator j n))"
apply(unfold Mul_Collector_def Mul_Mutator_def)
apply interfree_aux
apply(simp_all add:mul_collector_mutator_interfree)
apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
apply(tactic  ‹TRYALL (interfree_aux_tac 🍋)›)
🍋 ‹42 subgoals left›
apply (clarify,simp add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)+
🍋 ‹24 subgoals left›
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
🍋 ‹14 subgoals left›
apply(tactic ‹TRYALL (clarify_tac 🍋)›)
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic ‹TRYALL (resolve_tac 🍋 [conjI])›)
apply(tactic ‹TRYALL (resolve_tac 🍋 [impI])›)
apply(tactic ‹TRYALL (eresolve_tac 🍋 [disjE])›)
apply(tactic ‹TRYALL (eresolve_tac 🍋 [conjE])›)
apply(tactic ‹TRYALL (eresolve_tac 🍋 [disjE])›)
apply(tactic ‹TRYALL (eresolve_tac 🍋 [disjE])›)
🍋 ‹72 subgoals left›
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
🍋 ‹35 subgoals left›
apply(tactic ‹TRYALL(EVERY'[resolve_tac \<^context> [disjI1],
    resolve_tac 🍋 @{thms subset_trans},
    eresolve_tac 🍋 @{thms Graph3},
    force_tac 🍋,
    assume_tac 🍋])›)
🍋 ‹28 subgoals left›
apply(tactic ‹TRYALL (eresolve_tac 🍋 [conjE])›)
apply(tactic ‹TRYALL (eresolve_tac 🍋 [disjE])›)
🍋 ‹34 subgoals left›
apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
apply(simp_all add:Graph10)
🍋 ‹47 subgoals left›
apply(tactic ‹TRYALL(EVERY'[REPEAT o resolve_tac \<^context> [disjI2],
    eresolve_tac 🍋 @{thms subset_psubset_trans},
    eresolve_tac 🍋 @{thms Graph11},
    force_tac 🍋])›)
🍋 ‹41 subgoals left›
apply(tactic ‹TRYALL(EVERY'[resolve_tac \<^context> [disjI2],
    resolve_tac 🍋 [disjI1],
    eresolve_tac 🍋 @{thms le_trans},
    force_tac (🍋 addsimps @{thms Queue_def less_Suc_eq_le le_length_filter_update})])›)
🍋 ‹35 subgoals left›
apply(tactic ‹TRYALL(EVERY'[resolve_tac \<^context> [disjI2],
    resolve_tac 🍋 [disjI1],
    eresolve_tac 🍋 @{thms psubset_subset_trans},
    resolve_tac 🍋 @{thms Graph9},
    force_tac 🍋])›)
🍋 ‹31 subgoals left›
apply(tactic ‹TRYALL(EVERY'[resolve_tac \<^context> [disjI2],
    resolve_tac 🍋 [disjI1],
    eresolve_tac 🍋 @{thms subset_psubset_trans},
    eresolve_tac 🍋 @{thms Graph11},
    force_tac 🍋])›)
🍋 ‹29 subgoals left›
apply(tactic ‹TRYALL(EVERY'[REPEAT o resolve_tac \<^context> [disjI2],
    eresolve_tac 🍋 @{thms subset_psubset_trans},
    eresolve_tac 🍋 @{thms subset_psubset_trans},
    eresolve_tac 🍋 @{thms Graph11},
    force_tac 🍋])›)
🍋 ‹25 subgoals left›
apply(tactic ‹TRYALL(EVERY'[resolve_tac \<^context> [disjI2],
    resolve_tac 🍋 [disjI2],
    resolve_tac 🍋 [disjI1],
    eresolve_tac 🍋 @{thms le_trans},
    force_tac (🍋 addsimps @{thms Queue_def less_Suc_eq_le le_length_filter_update})])›)
🍋 ‹10 subgoals left›
apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+
done

subsubsection ‹Interference freedom Mutator-Collector›

lemma Mul_interfree_Mutator_Collector: " j < n \
  interfree_aux (Some (Mul_Mutator j n), {}, Some (Mul_Collector n))"
apply(unfold Mul_Collector_def Mul_Mutator_def)
apply interfree_aux
apply(simp_all add:mul_collector_mutator_interfree)
apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
apply(tactic  ‹TRYALL (interfree_aux_tac 🍋)›)
🍋 ‹76 subgoals left›
apply (clarsimp simp add: nth_list_update)+
🍋 ‹56 subgoals left›
apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
done

subsubsection ‹The Multi-Mutator Garbage Collection Algorithm›

text ‹The total number of verification conditions is 328›

lemma Mul_Gar_Coll:
 "\- \\Mul_Proper n \ \Mul_mut_init n \ (\iMuts!i))\
 COBEGIN
  Mul_Collector n
 {False}
 ∥
 SCHEME  [0≤ j< n]
  Mul_Mutator j n
 {False}
 COEND
 {False}"
apply oghoare
🍋 ‹Strengthening the precondition›
apply(rule Int_greatest)
 apply (case_tac n)
  apply(force simp add: Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
 apply(simp add: Mul_Mutator_def mul_collector_defs mul_mutator_defs nth_append)
 apply force
apply clarify
apply(case_tac i)
 apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt)
🍋 ‹Collector›
apply(rule Mul_Collector)
🍋 ‹Mutator›
apply(erule Mul_Mutator)
🍋 ‹Interference freedom›
apply(simp add:Mul_interfree_Collector_Mutator)
apply(simp add:Mul_interfree_Mutator_Collector)
apply(simp add:Mul_interfree_Mutator_Mutator)
🍋 ‹Weakening of the postcondition›
apply(case_tac n)
 apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
apply(simp add:Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append)
done

end