# Theory Mul_Gar_Coll

theory Mul_Gar_Coll
imports Graph OG_Syntax
```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 ≡
⦃´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<n ⟹
⊢ Mul_Redirect_Edge j n
pre(Mul_Color_Target j n)"
apply (unfold mul_mutator_defs)
apply annhoare
apply(simp_all)
apply clarify
done

lemma Mul_Color_Target: "0≤j ∧ j<n ⟹
⊢  Mul_Color_Target j n
⦃´Mul_mut_init n ∧ Z (´Muts!j)⦄"
apply (unfold mul_mutator_defs)
apply annhoare
apply(simp_all)
apply clarify
done

lemma Mul_Mutator: "0≤j ∧ j<n ⟹
⊢ Mul_Mutator j n ⦃False⦄"
apply(unfold Mul_Mutator_def)
apply annhoare
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
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
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
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
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(tactic ‹TRYALL (interfree_aux_tac @{context})›)
apply(tactic ‹ALLGOALS (clarify_tac @{context})›)
done

subsubsection ‹Modular Parameterized Mutators›

lemma Mul_Parameterized_Mutators: "0<n ⟹
∥- ⦃´Mul_mut_init n ∧ (∀i<n. Z (´Muts!i))⦄
COBEGIN
SCHEME  [0≤ j< n]
Mul_Mutator j n
⦃False⦄
COEND
⦃False⦄"
apply oghoare
apply(erule Mul_Mutator)
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 safe
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
―‹4 subgoals left›
apply clarify
apply(simp add: mul_collector_defs Graph12 Graph6 Graph7 Graph8)
apply(disjE_tac)
apply(case_tac "M x! k x=Black")
apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
apply(case_tac "M x! k x=Black")
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
―‹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 ≡
⦃´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 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)
―‹2 subgoals left›
apply force
―‹1 subgoal left›
apply clarify
apply(drule_tac x = "ind x" in le_imp_less_or_eq)
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 ≡
⦃´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
Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply force
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 force
apply force
apply force
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
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
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(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(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(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(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(rule conjI)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
―‹4 subgoals left›
apply clarify
apply(disjE_tac)
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(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(rule conjI)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
―‹3 subgoals left›
apply clarify
apply(disjE_tac)
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(case_tac "R (Muts x ! j)= ind x")
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(case_tac "R (Muts x ! j)= ind x")
apply(rule impI)
apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
apply(rule conjI)
apply(rule impI)
apply(rule conjI)
apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
apply(case_tac "R (Muts x ! j)= ind x")
apply(rule impI)
apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
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(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(rule impI,rule conjI)
apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
apply(case_tac "R (Muts x! j)=ind x")
apply(rule impI, (rule disjI2)+, erule le_trans)
―‹2 subgoals left›
apply clarify
apply(rule conjI)
apply(disjE_tac)
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(case_tac "R (Muts x ! j)= ind x")
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(case_tac "R (Muts x ! j)= ind x")
apply(rule impI)
apply(rule conjI)
apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
apply(case_tac "R (Muts x ! j)= ind x")
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(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(rule impI)
apply simp
apply(disjE_tac)
apply(rule disjI1, erule less_le_trans)
apply force
apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
apply(case_tac "R (Muts x ! j)= ind x")
apply(disjE_tac)
apply simp_all
apply(conjI_tac)
apply(rule impI)
apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
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
―‹1 subgoal left›
apply clarify
apply(disjE_tac)
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(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(rule conjI)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
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
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
―‹7 subgoals left›
apply clarify
apply(disjE_tac)
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(disjE_tac)
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(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(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(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(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(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)
―‹2 subgoals left›
apply clarify
apply(case_tac "M x!(T (Muts x!j))=Black")
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)
―‹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(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
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 clarify
apply disjE_tac
apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply clarify
apply disjE_tac
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)
―‹8 subgoals left›
―‹7 subgoals left›
apply clarify
apply disjE_tac
apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply clarify
apply disjE_tac
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)
―‹6 subgoals left›
apply clarify
apply disjE_tac
apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply clarify
apply disjE_tac
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)
―‹5 subgoals left›
apply clarify
apply disjE_tac
apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply clarify
apply disjE_tac
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)
―‹4 subgoals left›
apply clarify
apply disjE_tac
apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply clarify
apply disjE_tac
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)
―‹3 subgoals left›
―‹2 subgoals left›
apply clarify
apply disjE_tac
apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
apply clarify
apply disjE_tac
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)
―‹1 subgoal left›
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
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
―‹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: Graph7 Graph8 Graph12)
apply(rule conjI)
apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
―‹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
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})›)
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(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 (resolve_tac @{context} [conjI])›)
apply(tactic ‹TRYALL (resolve_tac @{context} [impI])›)
apply(tactic ‹TRYALL (eresolve_tac @{context} [disjE])›)
apply(tactic ‹TRYALL (eresolve_tac @{context} [conjE])›)
apply(tactic ‹TRYALL (eresolve_tac @{context} [disjE])›)
apply(tactic ‹TRYALL (eresolve_tac @{context} [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 @{context} [subset_trans],
eresolve_tac @{context} @{thms Graph3},
force_tac @{context},
assume_tac @{context}])›)
―‹28 subgoals left›
apply(tactic ‹TRYALL (eresolve_tac @{context} [conjE])›)
apply(tactic ‹TRYALL (eresolve_tac @{context} [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")
―‹47 subgoals left›
apply(tactic ‹TRYALL(EVERY'[REPEAT o resolve_tac @{context} [disjI2],
eresolve_tac @{context} @{thms subset_psubset_trans},
eresolve_tac @{context} @{thms Graph11},
force_tac @{context}])›)
―‹41 subgoals left›
apply(tactic ‹TRYALL(EVERY'[resolve_tac @{context} [disjI2],
resolve_tac @{context} [disjI1],
eresolve_tac @{context} @{thms le_trans},
force_tac (@{context} 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 @{context} [disjI1],
eresolve_tac @{context} @{thms psubset_subset_trans},
resolve_tac @{context} @{thms Graph9},
force_tac @{context}])›)
―‹31 subgoals left›
apply(tactic ‹TRYALL(EVERY'[resolve_tac @{context} [disjI2],
resolve_tac @{context} [disjI1],
eresolve_tac @{context} @{thms subset_psubset_trans},
eresolve_tac @{context} @{thms Graph11},
force_tac @{context}])›)
―‹29 subgoals left›
apply(tactic ‹TRYALL(EVERY'[REPEAT o resolve_tac @{context} [disjI2],
eresolve_tac @{context} @{thms subset_psubset_trans},
eresolve_tac @{context} @{thms subset_psubset_trans},
eresolve_tac @{context} @{thms Graph11},
force_tac @{context}])›)
―‹25 subgoals left›
apply(tactic ‹TRYALL(EVERY'[resolve_tac @{context} [disjI2],
resolve_tac @{context} [disjI2],
resolve_tac @{context} [disjI1],
eresolve_tac @{context} @{thms le_trans},
force_tac (@{context} 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(unfold mul_modules mul_collector_defs mul_mutator_defs)
apply(tactic  ‹TRYALL (interfree_aux_tac @{context})›)
―‹76 subgoals left›
―‹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 ∧ (∀i<n. Z (´Muts!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_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›