Theory Mul_Gar_Coll

theory Mul_Gar_Coll
imports Graph OG_Syntax
header {* \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 ∧ (∀i<n. R (´Muts!i)<length ´E 
                          ∧ T (´Muts!i)<length ´M) »"

definition Mul_Redirect_Edge  :: "nat => nat => mul_gar_coll_state ann_com" where
  "Mul_Redirect_Edge j n ≡
  \<lbrace>´Mul_mut_init n ∧ Z (´Muts!j)\<rbrace>
  ⟨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 ≡
  \<lbrace>´Mul_mut_init n ∧ ¬ Z (´Muts!j)\<rbrace> 
  ⟨´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 ≡
  \<lbrace>´Mul_mut_init n ∧ Z (´Muts!j)\<rbrace>  
  WHILE True  
    INV \<lbrace>´Mul_mut_init n ∧ Z (´Muts!j)\<rbrace>  
  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<n ==> 
  \<turnstile> 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<n ==> 
  \<turnstile>  Mul_Color_Target j n  
    \<lbrace>´Mul_mut_init n ∧ Z (´Muts!j)\<rbrace>"
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<n ==>  
 \<turnstile> Mul_Mutator j n \<lbrace>False\<rbrace>"
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; i<n; 0≤j; j<n; i≠j|] ==>  
  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; i<n; 0≤j; j<n; i≠j|] ==>  
  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; i<n; 0≤j; j<n; i≠j|] ==> 
  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; i<n; 0≤j; j<n; i≠j|] ==> 
  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 @{context}) *})
apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
apply (simp_all add:nth_list_update)
done

subsubsection {* Modular Parameterized Mutators *}

lemma Mul_Parameterized_Mutators: "0<n ==>
 \<parallel>- \<lbrace>´Mul_mut_init n ∧ (∀i<n. Z (´Muts!i))\<rbrace>
 COBEGIN
 SCHEME  [0≤ j< n]
  Mul_Mutator j n
 \<lbrace>False\<rbrace>
 COEND
 \<lbrace>False\<rbrace>"
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 ≡
  \<lbrace>´Mul_Proper n\<rbrace>
  ´ind:=0;;
  \<lbrace>´Mul_Proper n ∧ ´ind=0\<rbrace>
  WHILE ´ind<length ´M 
    INV \<lbrace>´Mul_Proper n ∧ (∀i<´ind. i∈Roots --> ´M!i=Black) ∧ ´ind≤length ´M\<rbrace>
  DO \<lbrace>´Mul_Proper n ∧ (∀i<´ind. i∈Roots --> ´M!i=Black) ∧ ´ind<length ´M\<rbrace>
       IF ´ind∈Roots THEN 
     \<lbrace>´Mul_Proper n ∧ (∀i<´ind. i∈Roots --> ´M!i=Black) ∧ ´ind<length ´M ∧ ´ind∈Roots\<rbrace> 
       ´M:=´M[´ind:=Black] FI;;
     \<lbrace>´Mul_Proper n ∧ (∀i<´ind+1. i∈Roots --> ´M!i=Black) ∧ ´ind<length ´M\<rbrace>
       ´ind:=´ind+1 
  OD"

lemma Mul_Blacken_Roots: 
  "\<turnstile> Mul_Blacken_Roots n  
  \<lbrace>´Mul_Proper n ∧ Roots ⊆ Blacks ´M\<rbrace>"
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 ≡
 \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
  ∧ (´Safe ∨ ´l≤´Queue ∨ ´obc⊂Blacks ´M)\<rbrace> 
 ´ind:=0;;
 \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M 
   ∧ ´obc⊆Blacks ´M ∧ Blacks ´M⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
   ∧ (´Safe ∨ ´l≤´Queue ∨ ´obc⊂Blacks ´M) ∧ ´ind=0\<rbrace> 
 WHILE ´ind<length ´E 
  INV \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M 
        ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
        ∧ ´Mul_PBInv ∧ ´ind≤length ´E\<rbrace>
 DO \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M 
     ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
     ∧ ´Mul_PBInv ∧ ´ind<length ´E\<rbrace>
   IF ´M!(fst (´E!´ind))=Black THEN 
   \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M 
     ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
     ∧ ´Mul_PBInv ∧ (´M!fst(´E!´ind))=Black ∧ ´ind<length ´E\<rbrace>
    ´k:=snd(´E!´ind);;
   \<lbrace>´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\<rbrace>
   ⟨´M:=´M[´k:=Black],,´ind:=´ind+1⟩
   ELSE \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M 
         ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
         ∧ ´Mul_PBInv ∧ ´ind<length ´E\<rbrace>
         ⟨IF ´M!(fst (´E!´ind))≠Black THEN ´ind:=´ind+1 FI⟩ FI
 OD"

lemma Mul_Propagate_Black: 
  "\<turnstile> Mul_Propagate_Black n  
   \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
     ∧ (´Safe ∨ ´obc⊂Blacks ´M ∨ ´l<´Queue ∧ (´l≤´Queue ∨ ´obc⊂Blacks ´M))\<rbrace>"
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<ind ∧ ´Ma!i=Black}⊆´bc »"

definition Mul_Count :: "nat =>  mul_gar_coll_state ann_com" where
  "Mul_Count n ≡ 
  \<lbrace>´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={}\<rbrace>
  ´ind:=0;;
  \<lbrace>´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\<rbrace>
  WHILE ´ind<length ´M 
     INV \<lbrace>´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\<rbrace>
  DO \<lbrace>´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\<rbrace> 
     IF ´M!´ind=Black 
     THEN \<lbrace>´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\<rbrace>
          ´bc:=insert ´ind ´bc
     FI;;
  \<lbrace>´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\<rbrace>
  ´ind:=´ind+1
  OD"
 
lemma Mul_Count: 
  "\<turnstile> Mul_Count n  
  \<lbrace>´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\<rbrace>"
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 --> i<length ´M --> i∈Reach ´E --> ´M!i=Black)»"

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

lemma Mul_Append: 
  "\<turnstile> Mul_Append n  
     \<lbrace>´Mul_Proper n\<rbrace>"
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 ≡
\<lbrace>´Mul_Proper n\<rbrace>  
WHILE True INV \<lbrace>´Mul_Proper n\<rbrace> 
DO  
Mul_Blacken_Roots n ;; 
\<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M\<rbrace>  
 ´obc:={};; 
\<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc={}\<rbrace>  
 ´bc:=Roots;; 
\<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc={} ∧ ´bc=Roots\<rbrace> 
 ´l:=0;; 
\<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´obc={} ∧ ´bc=Roots ∧ ´l=0\<rbrace> 
 WHILE ´l<n+1  
   INV \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´bc⊆Blacks ´M ∧  
         (´Safe ∨ (´l≤´Queue ∨ ´bc⊂Blacks ´M) ∧ ´l<n+1)\<rbrace> 
 DO \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
      ∧ (´Safe ∨ ´l≤´Queue ∨ ´bc⊂Blacks ´M)\<rbrace>
    ´obc:=´bc;;
    Mul_Propagate_Black n;; 
    \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M 
      ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
      ∧ (´Safe ∨ ´obc⊂Blacks ´M ∨ ´l<´Queue 
      ∧ (´l≤´Queue ∨ ´obc⊂Blacks ´M))\<rbrace> 
    ´bc:={};;
    \<lbrace>´Mul_Proper n ∧ Roots⊆Blacks ´M 
      ∧ ´obc⊆Blacks ´M ∧ ´bc⊆Blacks ´M 
      ∧ (´Safe ∨ ´obc⊂Blacks ´M ∨ ´l<´Queue 
      ∧ (´l≤´Queue ∨ ´obc⊂Blacks ´M)) ∧ ´bc={}\<rbrace> 
       ⟨ ´Ma:=´M,, ´q:=´Queue ⟩;;
    Mul_Count n;; 
    \<lbrace>´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\<rbrace> 
    IF ´obc=´bc THEN
    \<lbrace>´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\<rbrace>  
    ´l:=´l+1  
    ELSE \<lbrace>´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\<rbrace>  
        ´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:
  "\<turnstile> Mul_Collector n 
  \<lbrace>False\<rbrace>"
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 list 
 --> 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 list 
 --> 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<n|] ==>  
  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<n|]==> 
  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<n|]==>  
  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<n|]==>  
  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<n|]==>  
  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<n|]==>  
  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<n|]==>  
  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<n|]==>  
  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<n|]==>  
  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<n|]==>  
  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<n|]==>  
  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<n|]==>  
  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<n|]==>  
  interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
apply (unfold mul_modules)
apply interfree_aux
apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
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<n|]==>  
  interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
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<n|]==>  
  interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
apply (unfold mul_modules)
apply interfree_aux
apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
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<n|]==>  
  interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
apply(tactic {* ALLGOALS (clarify_tac @{context}) *})
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<n  ==> 
  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 @{context}) *})
--{* 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 @{context}) *})
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (rtac conjI) *})
apply(tactic {* TRYALL (rtac impI) *})
apply(tactic {* TRYALL (etac disjE) *})
apply(tactic {* TRYALL (etac conjE) *})
apply(tactic {* TRYALL (etac disjE) *})
apply(tactic {* TRYALL (etac 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'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac]) *})
--{* 28 subgoals left *}
apply(tactic {* TRYALL (etac conjE) *})
apply(tactic {* TRYALL (etac 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 (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}]) *})
--{* 41 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans},
    force_tac (@{context} addsimps
      [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
--{* 35 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}]) *})
--{* 31 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
--{* 29 subgoals left *}
apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}]) *})
--{* 25 subgoals left *}
apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans},
    force_tac (@{context} addsimps
      [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm 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 @{context}) *})
--{* 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: 
 "\<parallel>- \<lbrace>´Mul_Proper n ∧ ´Mul_mut_init n ∧ (∀i<n. Z (´Muts!i))\<rbrace>  
 COBEGIN  
  Mul_Collector n
 \<lbrace>False\<rbrace>
 \<parallel>  
 SCHEME  [0≤ j< n]
  Mul_Mutator j n
 \<lbrace>False\<rbrace>  
 COEND  
 \<lbrace>False\<rbrace>"
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