Up to index of Isabelle/HOL/HoareParallel
theory Mul_Gar_Collheader {* \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 *} constdefs Mul_mut_init :: "mul_gar_coll_state => nat => bool" "Mul_mut_init ≡ « λn. n=length ´Muts ∧ (∀i<n. R (´Muts!i)<length ´E ∧ T (´Muts!i)<length ´M) »" Mul_Redirect_Edge :: "nat => nat => mul_gar_coll_state ann_com" "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|)),]〉" Mul_Color_Target :: "nat => nat => mul_gar_coll_state ann_com" "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|)),]〉" Mul_Mutator :: "nat => nat => mul_gar_coll_state ann_com" "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 ==> \<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 .{´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<n ==> \<turnstile> 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; 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) *}) apply(tactic {* ALLGOALS Clarify_tac *}) apply (simp_all add:nth_list_update) done subsubsection {* Modular Parameterized Mutators *} lemma Mul_Parameterized_Mutators: "0<n ==> \<parallel>- .{´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 *} constdefs Queue :: "mul_gar_coll_state => nat" "Queue ≡ « length (filter (λi. ¬ Z i ∧ ´M!(T i) ≠ Black) ´Muts) »" consts M_init :: nodes constdefs Proper_M_init :: "mul_gar_coll_state => bool" "Proper_M_init ≡ « Blacks M_init=Roots ∧ length M_init=length ´M »" Mul_Proper :: "mul_gar_coll_state => nat => bool" "Mul_Proper ≡ « λn. Proper_Roots ´M ∧ Proper_Edges (´M, ´E) ∧ ´Proper_M_init ∧ n=length ´Muts »" Safe :: "mul_gar_coll_state => bool" "Safe ≡ « Reach ´E ⊆ Blacks ´M »" lemmas mul_collector_defs = Proper_M_init_def Mul_Proper_def Safe_def subsubsection {* Blackening Roots *} constdefs Mul_Blacken_Roots :: "nat => mul_gar_coll_state ann_com" "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: "\<turnstile> 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 *} constdefs Mul_PBInv :: "mul_gar_coll_state => bool" "Mul_PBInv ≡ «´Safe ∨ ´obc⊂Blacks ´M ∨ ´l<´Queue ∨ (∀i<´ind. ¬BtoW(´E!i,´M)) ∧ ´l≤´Queue»" Mul_Auxk :: "mul_gar_coll_state => bool" "Mul_Auxk ≡ «´l<´Queue ∨ ´M!´k≠Black ∨ ¬BtoW(´E!´ind, ´M) ∨ ´obc⊂Blacks ´M»" constdefs Mul_Propagate_Black :: "nat => mul_gar_coll_state ann_com" "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: "\<turnstile> 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) --{* 3 subgoals left *} apply 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 *} constdefs Mul_CountInv :: "mul_gar_coll_state => nat => bool" "Mul_CountInv ≡ « λind. {i. i<ind ∧ ´Ma!i=Black}⊆´bc »" Mul_Count :: "nat => mul_gar_coll_state ann_com" "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: "\<turnstile> 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 le_imp_less_or_eq) apply(disjE_tac) apply (simp_all add:Blacks_def) done subsubsection {* Appending garbage nodes to the free list *} consts Append_to_free :: "nat × edges => edges" axioms Append_to_free0: "length (Append_to_free (i, e)) = length e" Append_to_free1: "Proper_Edges (m, e) ==> Proper_Edges (m, Append_to_free(i, e))" Append_to_free2: "i ∉ Reach e ==> n ∈ Reach (Append_to_free(i, e)) = ( n = i ∨ n ∈ Reach e)" constdefs Mul_AppendInv :: "mul_gar_coll_state => nat => bool" "Mul_AppendInv ≡ « λind. (∀i. ind≤i --> i<length ´M --> i∈Reach ´E --> ´M!i=Black)»" Mul_Append :: "nat => mul_gar_coll_state ann_com" "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: "\<turnstile> 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 *} constdefs Mul_Collector :: "nat => mul_gar_coll_state ann_com" "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: "\<turnstile> 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 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 *}) 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 *}) 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 *}) 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 *}) 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) *}) --{* 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 (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, 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(tactic {* ALLGOALS(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 subset_psubset_trans,etac (thm "Graph11"),Force_tac]) *}) --{* 41 subgoals left *} apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", less_Suc_eq_le, thm "le_length_filter_update"])]) *}) --{* 35 subgoals left *} apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac psubset_subset_trans,rtac (thm "Graph9"),Force_tac]) *}) --{* 31 subgoals left *} apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac subset_psubset_trans,etac (thm "Graph11"),Force_tac]) *}) --{* 29 subgoals left *} apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac subset_psubset_trans,etac subset_psubset_trans,etac (thm "Graph11"),Force_tac]) *}) --{* 25 subgoals left *} apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac le_trans, force_tac (claset(),simpset() addsimps [thm "Queue_def", 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) *}) --{* 76 subgoals left *} apply (clarify,simp add: nth_list_update)+ --{* 56 subgoals left *} apply(clarify,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>- .{´Mul_Proper n ∧ ´Mul_mut_init n ∧ (∀i<n. Z (´Muts!i))}. COBEGIN Mul_Collector n .{False}. \<parallel> 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 xa) 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
lemmas mul_mutator_defs:
Mul_mut_init == %s n. n = length (Muts s) ∧ (∀i<n. R (Muts s ! i) < length (E s) ∧ T (Muts s ! i) < length (M s))
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 |)]〉
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 |)]〉
lemmas mul_mutator_defs:
Mul_mut_init == %s n. n = length (Muts s) ∧ (∀i<n. R (Muts s ! i) < length (E s) ∧ T (Muts s ! i) < length (M s))
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 |)]〉
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 |)]〉
lemma Mul_Redirect_Edge:
0 ≤ j ∧ j < n ==> \<turnstile> Mul_Redirect_Edge j n pre (Mul_Color_Target j n)
lemma Mul_Color_Target:
0 ≤ j ∧ j < n ==> \<turnstile> Mul_Color_Target j n .{´Mul_mut_init n ∧ Z (´Muts ! j)}.
lemma Mul_Mutator:
0 ≤ j ∧ j < n ==> \<turnstile> Mul_Mutator j n .{False}.
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))
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))
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))
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))
lemmas mul_mutator_interfree:
[| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |] ==> interfree_aux (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |] ==> interfree_aux (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |] ==> interfree_aux (Some (Mul_Color_Target i n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |] ==> interfree_aux (Some (Mul_Color_Target i n), {}, Some (Mul_Color_Target j n))
lemmas mul_mutator_interfree:
[| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |] ==> interfree_aux (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |] ==> interfree_aux (Some (Mul_Redirect_Edge i n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |] ==> interfree_aux (Some (Mul_Color_Target i n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ i; i < n; 0 ≤ j; j < n; i ≠ j |] ==> interfree_aux (Some (Mul_Color_Target i n), {}, Some (Mul_Color_Target j n))
lemma Mul_interfree_Mutator_Mutator:
[| i < n; j < n; i ≠ j |] ==> interfree_aux (Some (Mul_Mutator i n), {}, Some (Mul_Mutator j n))
lemma Mul_Parameterized_Mutators:
0 < n ==> \<parallel>- .{´Mul_mut_init n ∧ (∀i<n. Z (´Muts ! i))}. COBEGIN SCHEME [0 ≤ j < n] Mul_Mutator j n .{False}. COEND .{False}.
lemmas mul_collector_defs:
Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
Mul_Proper == %s n. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s ∧ n = length (Muts s)
Safe == %s. Reach (E s) ⊆ Blacks (M s)
lemmas mul_collector_defs:
Proper_M_init == %s. Blacks M_init = Roots ∧ length M_init = length (M s)
Mul_Proper == %s n. Proper_Roots (M s) ∧ Proper_Edges (M s, E s) ∧ Proper_M_init s ∧ n = length (Muts s)
Safe == %s. Reach (E s) ⊆ Blacks (M s)
lemma Mul_Blacken_Roots:
\<turnstile> Mul_Blacken_Roots n .{´Mul_Proper n ∧ Roots ⊆ Blacks ´M}.
lemma Mul_Propagate_Black:
\<turnstile> 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))}.
lemma Mul_Count:
\<turnstile> 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}.
lemma Mul_Append:
\<turnstile> Mul_Append n .{´Mul_Proper n}.
lemmas mul_modules:
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 |)]〉
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 |)]〉
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
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
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
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
lemmas mul_modules:
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 |)]〉
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 |)]〉
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
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
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
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_Collector:
\<turnstile> Mul_Collector n
.{False}.
lemma le_length_filter_update:
(¬ P (list ! i) ∨ P j) ∧ i < length list ==> length (filter P list) ≤ length (filter P (list[i := j]))
lemma less_length_filter_update:
P j ∧ ¬ P (list ! i) ∧ i < length list ==> length (filter P list) < length (filter P (list[i := j]))
lemma Mul_interfree_Blacken_Roots_Redirect_Edge:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Redirect_Edge j n))
lemma Mul_interfree_Redirect_Edge_Blacken_Roots:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Blacken_Roots n))
lemma Mul_interfree_Blacken_Roots_Color_Target:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Color_Target j n))
lemma Mul_interfree_Color_Target_Blacken_Roots:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Blacken_Roots n))
lemma Mul_interfree_Propagate_Black_Redirect_Edge:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Propagate_Black n), {}, Some (Mul_Redirect_Edge j n))
lemma Mul_interfree_Redirect_Edge_Propagate_Black:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Propagate_Black n))
lemma Mul_interfree_Propagate_Black_Color_Target:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Propagate_Black n), {}, Some (Mul_Color_Target j n))
lemma Mul_interfree_Color_Target_Propagate_Black:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Propagate_Black n))
lemma Mul_interfree_Count_Redirect_Edge:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Redirect_Edge j n))
lemma Mul_interfree_Redirect_Edge_Count:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Count n))
lemma Mul_interfree_Count_Color_Target:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Color_Target j n))
lemma Mul_interfree_Color_Target_Count:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Count n))
lemma Mul_interfree_Append_Redirect_Edge:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Redirect_Edge j n))
lemma Mul_interfree_Redirect_Edge_Append:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Append n))
lemma Mul_interfree_Append_Color_Target:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Color_Target j n))
lemma Mul_interfree_Color_Target_Append:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Append n))
lemmas mul_collector_mutator_interfree:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Propagate_Black n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Propagate_Black n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Blacken_Roots n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Blacken_Roots n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Propagate_Black n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Propagate_Black n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Count n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Count n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Append n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Append n))
lemmas mul_collector_mutator_interfree:
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Blacken_Roots n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Propagate_Black n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Propagate_Black n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Count n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Redirect_Edge j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Append n), {}, Some (Mul_Color_Target j n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Blacken_Roots n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Blacken_Roots n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Propagate_Black n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Propagate_Black n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Count n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Count n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Redirect_Edge j n), {}, Some (Mul_Append n))
[| 0 ≤ j; j < n |] ==> interfree_aux (Some (Mul_Color_Target j n), {}, Some (Mul_Append n))
lemma Mul_interfree_Collector_Mutator:
j < n ==> interfree_aux (Some (Mul_Collector n), {}, Some (Mul_Mutator j n))
lemma Mul_interfree_Mutator_Collector:
j < n ==> interfree_aux (Some (Mul_Mutator j n), {}, Some (Mul_Collector n))
lemma Mul_Gar_Coll:
\<parallel>- .{´Mul_Proper n ∧ ´Mul_mut_init n ∧ (∀i<n. Z (´Muts ! i))}. COBEGIN Mul_Collector n .{False}. \<parallel> SCHEME [0 ≤ j < n] Mul_Mutator j n .{False}. COEND .{False}.