src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
 author wenzelm Tue Jan 16 09:30:00 2018 +0100 (19 months ago) changeset 67443 3abf6a722518 parent 62042 6c6ccf573479 child 69597 ff784d5a5bfb permissions -rw-r--r--
```     1 section \<open>The Multi-Mutator Case\<close>
```
```     2
```
```     3 theory Mul_Gar_Coll imports Graph OG_Syntax begin
```
```     4
```
```     5 text \<open>The full theory takes aprox. 18 minutes.\<close>
```
```     6
```
```     7 record mut =
```
```     8   Z :: bool
```
```     9   R :: nat
```
```    10   T :: nat
```
```    11
```
```    12 text \<open>Declaration of variables:\<close>
```
```    13
```
```    14 record mul_gar_coll_state =
```
```    15   M :: nodes
```
```    16   E :: edges
```
```    17   bc :: "nat set"
```
```    18   obc :: "nat set"
```
```    19   Ma :: nodes
```
```    20   ind :: nat
```
```    21   k :: nat
```
```    22   q :: nat
```
```    23   l :: nat
```
```    24   Muts :: "mut list"
```
```    25
```
```    26 subsection \<open>The Mutators\<close>
```
```    27
```
```    28 definition Mul_mut_init :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
```
```    29   "Mul_mut_init \<equiv> \<guillemotleft> \<lambda>n. n=length \<acute>Muts \<and> (\<forall>i<n. R (\<acute>Muts!i)<length \<acute>E
```
```    30                           \<and> T (\<acute>Muts!i)<length \<acute>M) \<guillemotright>"
```
```    31
```
```    32 definition Mul_Redirect_Edge  :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com" where
```
```    33   "Mul_Redirect_Edge j n \<equiv>
```
```    34   \<lbrace>\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)\<rbrace>
```
```    35   \<langle>IF T(\<acute>Muts!j) \<in> Reach \<acute>E THEN
```
```    36   \<acute>E:= \<acute>E[R (\<acute>Muts!j):= (fst (\<acute>E!R(\<acute>Muts!j)), T (\<acute>Muts!j))] FI,,
```
```    37   \<acute>Muts:= \<acute>Muts[j:= (\<acute>Muts!j) \<lparr>Z:=False\<rparr>]\<rangle>"
```
```    38
```
```    39 definition Mul_Color_Target :: "nat \<Rightarrow> nat \<Rightarrow> mul_gar_coll_state ann_com" where
```
```    40   "Mul_Color_Target j n \<equiv>
```
```    41   \<lbrace>\<acute>Mul_mut_init n \<and> \<not> Z (\<acute>Muts!j)\<rbrace>
```
```    42   \<langle>\<acute>M:=\<acute>M[T (\<acute>Muts!j):=Black],, \<acute>Muts:=\<acute>Muts[j:= (\<acute>Muts!j) \<lparr>Z:=True\<rparr>]\<rangle>"
```
```    43
```
```    44 definition Mul_Mutator :: "nat \<Rightarrow> nat \<Rightarrow>  mul_gar_coll_state ann_com" where
```
```    45   "Mul_Mutator j n \<equiv>
```
```    46   \<lbrace>\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)\<rbrace>
```
```    47   WHILE True
```
```    48     INV \<lbrace>\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)\<rbrace>
```
```    49   DO Mul_Redirect_Edge j n ;;
```
```    50      Mul_Color_Target j n
```
```    51   OD"
```
```    52
```
```    53 lemmas mul_mutator_defs = Mul_mut_init_def Mul_Redirect_Edge_def Mul_Color_Target_def
```
```    54
```
```    55 subsubsection \<open>Correctness of the proof outline of one mutator\<close>
```
```    56
```
```    57 lemma Mul_Redirect_Edge: "0\<le>j \<and> j<n \<Longrightarrow>
```
```    58   \<turnstile> Mul_Redirect_Edge j n
```
```    59      pre(Mul_Color_Target j n)"
```
```    60 apply (unfold mul_mutator_defs)
```
```    61 apply annhoare
```
```    62 apply(simp_all)
```
```    63 apply clarify
```
```    64 apply(simp add:nth_list_update)
```
```    65 done
```
```    66
```
```    67 lemma Mul_Color_Target: "0\<le>j \<and> j<n \<Longrightarrow>
```
```    68   \<turnstile>  Mul_Color_Target j n
```
```    69     \<lbrace>\<acute>Mul_mut_init n \<and> Z (\<acute>Muts!j)\<rbrace>"
```
```    70 apply (unfold mul_mutator_defs)
```
```    71 apply annhoare
```
```    72 apply(simp_all)
```
```    73 apply clarify
```
```    74 apply(simp add:nth_list_update)
```
```    75 done
```
```    76
```
```    77 lemma Mul_Mutator: "0\<le>j \<and> j<n \<Longrightarrow>
```
```    78  \<turnstile> Mul_Mutator j n \<lbrace>False\<rbrace>"
```
```    79 apply(unfold Mul_Mutator_def)
```
```    80 apply annhoare
```
```    81 apply(simp_all add:Mul_Redirect_Edge Mul_Color_Target)
```
```    82 apply(simp add:mul_mutator_defs Mul_Redirect_Edge_def)
```
```    83 done
```
```    84
```
```    85 subsubsection \<open>Interference freedom between mutators\<close>
```
```    86
```
```    87 lemma Mul_interfree_Redirect_Edge_Redirect_Edge:
```
```    88   "\<lbrakk>0\<le>i; i<n; 0\<le>j; j<n; i\<noteq>j\<rbrakk> \<Longrightarrow>
```
```    89   interfree_aux (Some (Mul_Redirect_Edge i n),{}, Some(Mul_Redirect_Edge j n))"
```
```    90 apply (unfold mul_mutator_defs)
```
```    91 apply interfree_aux
```
```    92 apply safe
```
```    93 apply(simp_all add: nth_list_update)
```
```    94 done
```
```    95
```
```    96 lemma Mul_interfree_Redirect_Edge_Color_Target:
```
```    97   "\<lbrakk>0\<le>i; i<n; 0\<le>j; j<n; i\<noteq>j\<rbrakk> \<Longrightarrow>
```
```    98   interfree_aux (Some(Mul_Redirect_Edge i n),{},Some(Mul_Color_Target j n))"
```
```    99 apply (unfold mul_mutator_defs)
```
```   100 apply interfree_aux
```
```   101 apply safe
```
```   102 apply(simp_all add: nth_list_update)
```
```   103 done
```
```   104
```
```   105 lemma Mul_interfree_Color_Target_Redirect_Edge:
```
```   106   "\<lbrakk>0\<le>i; i<n; 0\<le>j; j<n; i\<noteq>j\<rbrakk> \<Longrightarrow>
```
```   107   interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Redirect_Edge j n))"
```
```   108 apply (unfold mul_mutator_defs)
```
```   109 apply interfree_aux
```
```   110 apply safe
```
```   111 apply(simp_all add:nth_list_update)
```
```   112 done
```
```   113
```
```   114 lemma Mul_interfree_Color_Target_Color_Target:
```
```   115   " \<lbrakk>0\<le>i; i<n; 0\<le>j; j<n; i\<noteq>j\<rbrakk> \<Longrightarrow>
```
```   116   interfree_aux (Some(Mul_Color_Target i n),{},Some(Mul_Color_Target j n))"
```
```   117 apply (unfold mul_mutator_defs)
```
```   118 apply interfree_aux
```
```   119 apply safe
```
```   120 apply(simp_all add: nth_list_update)
```
```   121 done
```
```   122
```
```   123 lemmas mul_mutator_interfree =
```
```   124   Mul_interfree_Redirect_Edge_Redirect_Edge Mul_interfree_Redirect_Edge_Color_Target
```
```   125   Mul_interfree_Color_Target_Redirect_Edge Mul_interfree_Color_Target_Color_Target
```
```   126
```
```   127 lemma Mul_interfree_Mutator_Mutator: "\<lbrakk>i < n; j < n; i \<noteq> j\<rbrakk> \<Longrightarrow>
```
```   128   interfree_aux (Some (Mul_Mutator i n), {}, Some (Mul_Mutator j n))"
```
```   129 apply(unfold Mul_Mutator_def)
```
```   130 apply(interfree_aux)
```
```   131 apply(simp_all add:mul_mutator_interfree)
```
```   132 apply(simp_all add: mul_mutator_defs)
```
```   133 apply(tactic \<open>TRYALL (interfree_aux_tac @{context})\<close>)
```
```   134 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```   135 apply (simp_all add:nth_list_update)
```
```   136 done
```
```   137
```
```   138 subsubsection \<open>Modular Parameterized Mutators\<close>
```
```   139
```
```   140 lemma Mul_Parameterized_Mutators: "0<n \<Longrightarrow>
```
```   141  \<parallel>- \<lbrace>\<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))\<rbrace>
```
```   142  COBEGIN
```
```   143  SCHEME  [0\<le> j< n]
```
```   144   Mul_Mutator j n
```
```   145  \<lbrace>False\<rbrace>
```
```   146  COEND
```
```   147  \<lbrace>False\<rbrace>"
```
```   148 apply oghoare
```
```   149 apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
```
```   150 apply(erule Mul_Mutator)
```
```   151 apply(simp add:Mul_interfree_Mutator_Mutator)
```
```   152 apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
```
```   153 done
```
```   154
```
```   155 subsection \<open>The Collector\<close>
```
```   156
```
```   157 definition Queue :: "mul_gar_coll_state \<Rightarrow> nat" where
```
```   158  "Queue \<equiv> \<guillemotleft> length (filter (\<lambda>i. \<not> Z i \<and> \<acute>M!(T i) \<noteq> Black) \<acute>Muts) \<guillemotright>"
```
```   159
```
```   160 consts  M_init :: nodes
```
```   161
```
```   162 definition Proper_M_init :: "mul_gar_coll_state \<Rightarrow> bool" where
```
```   163   "Proper_M_init \<equiv> \<guillemotleft> Blacks M_init=Roots \<and> length M_init=length \<acute>M \<guillemotright>"
```
```   164
```
```   165 definition Mul_Proper :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
```
```   166   "Mul_Proper \<equiv> \<guillemotleft> \<lambda>n. Proper_Roots \<acute>M \<and> Proper_Edges (\<acute>M, \<acute>E) \<and> \<acute>Proper_M_init \<and> n=length \<acute>Muts \<guillemotright>"
```
```   167
```
```   168 definition Safe :: "mul_gar_coll_state \<Rightarrow> bool" where
```
```   169   "Safe \<equiv> \<guillemotleft> Reach \<acute>E \<subseteq> Blacks \<acute>M \<guillemotright>"
```
```   170
```
```   171 lemmas mul_collector_defs = Proper_M_init_def Mul_Proper_def Safe_def
```
```   172
```
```   173 subsubsection \<open>Blackening Roots\<close>
```
```   174
```
```   175 definition Mul_Blacken_Roots :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
```
```   176   "Mul_Blacken_Roots n \<equiv>
```
```   177   \<lbrace>\<acute>Mul_Proper n\<rbrace>
```
```   178   \<acute>ind:=0;;
```
```   179   \<lbrace>\<acute>Mul_Proper n \<and> \<acute>ind=0\<rbrace>
```
```   180   WHILE \<acute>ind<length \<acute>M
```
```   181     INV \<lbrace>\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
```
```   182   DO \<lbrace>\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
```
```   183        IF \<acute>ind\<in>Roots THEN
```
```   184      \<lbrace>\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<in>Roots\<rbrace>
```
```   185        \<acute>M:=\<acute>M[\<acute>ind:=Black] FI;;
```
```   186      \<lbrace>\<acute>Mul_Proper n \<and> (\<forall>i<\<acute>ind+1. i\<in>Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
```
```   187        \<acute>ind:=\<acute>ind+1
```
```   188   OD"
```
```   189
```
```   190 lemma Mul_Blacken_Roots:
```
```   191   "\<turnstile> Mul_Blacken_Roots n
```
```   192   \<lbrace>\<acute>Mul_Proper n \<and> Roots \<subseteq> Blacks \<acute>M\<rbrace>"
```
```   193 apply (unfold Mul_Blacken_Roots_def)
```
```   194 apply annhoare
```
```   195 apply(simp_all add:mul_collector_defs Graph_defs)
```
```   196 apply safe
```
```   197 apply(simp_all add:nth_list_update)
```
```   198   apply (erule less_SucE)
```
```   199    apply simp+
```
```   200  apply force
```
```   201 apply force
```
```   202 done
```
```   203
```
```   204 subsubsection \<open>Propagating Black\<close>
```
```   205
```
```   206 definition Mul_PBInv :: "mul_gar_coll_state \<Rightarrow> bool" where
```
```   207   "Mul_PBInv \<equiv>  \<guillemotleft>\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue
```
```   208                  \<or> (\<forall>i<\<acute>ind. \<not>BtoW(\<acute>E!i,\<acute>M)) \<and> \<acute>l\<le>\<acute>Queue\<guillemotright>"
```
```   209
```
```   210 definition Mul_Auxk :: "mul_gar_coll_state \<Rightarrow> bool" where
```
```   211   "Mul_Auxk \<equiv> \<guillemotleft>\<acute>l<\<acute>Queue \<or> \<acute>M!\<acute>k\<noteq>Black \<or> \<not>BtoW(\<acute>E!\<acute>ind, \<acute>M) \<or> \<acute>obc\<subset>Blacks \<acute>M\<guillemotright>"
```
```   212
```
```   213 definition Mul_Propagate_Black :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
```
```   214   "Mul_Propagate_Black n \<equiv>
```
```   215  \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   216   \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)\<rbrace>
```
```   217  \<acute>ind:=0;;
```
```   218  \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   219    \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> Blacks \<acute>M\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   220    \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) \<and> \<acute>ind=0\<rbrace>
```
```   221  WHILE \<acute>ind<length \<acute>E
```
```   222   INV \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   223         \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   224         \<and> \<acute>Mul_PBInv \<and> \<acute>ind\<le>length \<acute>E\<rbrace>
```
```   225  DO \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   226      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   227      \<and> \<acute>Mul_PBInv \<and> \<acute>ind<length \<acute>E\<rbrace>
```
```   228    IF \<acute>M!(fst (\<acute>E!\<acute>ind))=Black THEN
```
```   229    \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   230      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   231      \<and> \<acute>Mul_PBInv \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black \<and> \<acute>ind<length \<acute>E\<rbrace>
```
```   232     \<acute>k:=snd(\<acute>E!\<acute>ind);;
```
```   233    \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   234      \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   235      \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue \<or> (\<forall>i<\<acute>ind. \<not>BtoW(\<acute>E!i,\<acute>M))
```
```   236         \<and> \<acute>l\<le>\<acute>Queue \<and> \<acute>Mul_Auxk ) \<and> \<acute>k<length \<acute>M \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black
```
```   237      \<and> \<acute>ind<length \<acute>E\<rbrace>
```
```   238    \<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],,\<acute>ind:=\<acute>ind+1\<rangle>
```
```   239    ELSE \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   240          \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   241          \<and> \<acute>Mul_PBInv \<and> \<acute>ind<length \<acute>E\<rbrace>
```
```   242          \<langle>IF \<acute>M!(fst (\<acute>E!\<acute>ind))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle> FI
```
```   243  OD"
```
```   244
```
```   245 lemma Mul_Propagate_Black:
```
```   246   "\<turnstile> Mul_Propagate_Black n
```
```   247    \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   248      \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))\<rbrace>"
```
```   249 apply(unfold Mul_Propagate_Black_def)
```
```   250 apply annhoare
```
```   251 apply(simp_all add:Mul_PBInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
```
```   252 \<comment> \<open>8 subgoals left\<close>
```
```   253 apply force
```
```   254 apply force
```
```   255 apply force
```
```   256 apply(force simp add:BtoW_def Graph_defs)
```
```   257 \<comment> \<open>4 subgoals left\<close>
```
```   258 apply clarify
```
```   259 apply(simp add: mul_collector_defs Graph12 Graph6 Graph7 Graph8)
```
```   260 apply(disjE_tac)
```
```   261  apply(simp_all add:Graph12 Graph13)
```
```   262  apply(case_tac "M x! k x=Black")
```
```   263   apply(simp add: Graph10)
```
```   264  apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
```
```   265 apply(case_tac "M x! k x=Black")
```
```   266  apply(simp add: Graph10 BtoW_def)
```
```   267  apply(rule disjI2, clarify, erule less_SucE, force)
```
```   268  apply(case_tac "M x!snd(E x! ind x)=Black")
```
```   269   apply(force)
```
```   270  apply(force)
```
```   271 apply(rule disjI2, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
```
```   272 \<comment> \<open>2 subgoals left\<close>
```
```   273 apply clarify
```
```   274 apply(conjI_tac)
```
```   275 apply(disjE_tac)
```
```   276  apply (simp_all)
```
```   277 apply clarify
```
```   278 apply(erule less_SucE)
```
```   279  apply force
```
```   280 apply (simp add:BtoW_def)
```
```   281 \<comment> \<open>1 subgoal left\<close>
```
```   282 apply clarify
```
```   283 apply simp
```
```   284 apply(disjE_tac)
```
```   285 apply (simp_all)
```
```   286 apply(rule disjI1 , rule Graph1)
```
```   287  apply simp_all
```
```   288 done
```
```   289
```
```   290 subsubsection \<open>Counting Black Nodes\<close>
```
```   291
```
```   292 definition Mul_CountInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
```
```   293   "Mul_CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>"
```
```   294
```
```   295 definition Mul_Count :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
```
```   296   "Mul_Count n \<equiv>
```
```   297   \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   298     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   299     \<and> length \<acute>Ma=length \<acute>M
```
```   300     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) )
```
```   301     \<and> \<acute>q<n+1 \<and> \<acute>bc={}\<rbrace>
```
```   302   \<acute>ind:=0;;
```
```   303   \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   304     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   305     \<and> length \<acute>Ma=length \<acute>M
```
```   306     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M) )
```
```   307     \<and> \<acute>q<n+1 \<and> \<acute>bc={} \<and> \<acute>ind=0\<rbrace>
```
```   308   WHILE \<acute>ind<length \<acute>M
```
```   309      INV \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   310           \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   311           \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind
```
```   312           \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
```
```   313           \<and> \<acute>q<n+1 \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
```
```   314   DO \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   315        \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   316        \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind
```
```   317        \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
```
```   318        \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M\<rbrace>
```
```   319      IF \<acute>M!\<acute>ind=Black
```
```   320      THEN \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   321             \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   322             \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv \<acute>ind
```
```   323             \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
```
```   324             \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace>
```
```   325           \<acute>bc:=insert \<acute>ind \<acute>bc
```
```   326      FI;;
```
```   327   \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   328     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   329     \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>Mul_CountInv (\<acute>ind+1)
```
```   330     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
```
```   331     \<and> \<acute>q<n+1 \<and> \<acute>ind<length \<acute>M\<rbrace>
```
```   332   \<acute>ind:=\<acute>ind+1
```
```   333   OD"
```
```   334
```
```   335 lemma Mul_Count:
```
```   336   "\<turnstile> Mul_Count n
```
```   337   \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   338     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   339     \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc
```
```   340     \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
```
```   341     \<and> \<acute>q<n+1\<rbrace>"
```
```   342 apply (unfold Mul_Count_def)
```
```   343 apply annhoare
```
```   344 apply(simp_all add:Mul_CountInv_def mul_collector_defs Mul_Auxk_def Graph6 Graph7 Graph8 Graph12 mul_collector_defs Queue_def)
```
```   345 \<comment> \<open>7 subgoals left\<close>
```
```   346 apply force
```
```   347 apply force
```
```   348 apply force
```
```   349 \<comment> \<open>4 subgoals left\<close>
```
```   350 apply clarify
```
```   351 apply(conjI_tac)
```
```   352 apply(disjE_tac)
```
```   353  apply simp_all
```
```   354 apply(simp add:Blacks_def)
```
```   355 apply clarify
```
```   356 apply(erule less_SucE)
```
```   357  back
```
```   358  apply force
```
```   359 apply force
```
```   360 \<comment> \<open>3 subgoals left\<close>
```
```   361 apply clarify
```
```   362 apply(conjI_tac)
```
```   363 apply(disjE_tac)
```
```   364  apply simp_all
```
```   365 apply clarify
```
```   366 apply(erule less_SucE)
```
```   367  back
```
```   368  apply force
```
```   369 apply simp
```
```   370 apply(rotate_tac -1)
```
```   371 apply (force simp add:Blacks_def)
```
```   372 \<comment> \<open>2 subgoals left\<close>
```
```   373 apply force
```
```   374 \<comment> \<open>1 subgoal left\<close>
```
```   375 apply clarify
```
```   376 apply(drule_tac x = "ind x" in le_imp_less_or_eq)
```
```   377 apply (simp_all add:Blacks_def)
```
```   378 done
```
```   379
```
```   380 subsubsection \<open>Appending garbage nodes to the free list\<close>
```
```   381
```
```   382 axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
```
```   383 where
```
```   384   Append_to_free0: "length (Append_to_free (i, e)) = length e" and
```
```   385   Append_to_free1: "Proper_Edges (m, e)
```
```   386                     \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and
```
```   387   Append_to_free2: "i \<notin> Reach e
```
```   388            \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
```
```   389
```
```   390 definition Mul_AppendInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
```
```   391   "Mul_AppendInv \<equiv> \<guillemotleft> \<lambda>ind. (\<forall>i. ind\<le>i \<longrightarrow> i<length \<acute>M \<longrightarrow> i\<in>Reach \<acute>E \<longrightarrow> \<acute>M!i=Black)\<guillemotright>"
```
```   392
```
```   393 definition Mul_Append :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
```
```   394   "Mul_Append n \<equiv>
```
```   395   \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe\<rbrace>
```
```   396   \<acute>ind:=0;;
```
```   397   \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0\<rbrace>
```
```   398   WHILE \<acute>ind<length \<acute>M
```
```   399     INV \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
```
```   400   DO \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M\<rbrace>
```
```   401       IF \<acute>M!\<acute>ind=Black THEN
```
```   402      \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace>
```
```   403       \<acute>M:=\<acute>M[\<acute>ind:=White]
```
```   404       ELSE
```
```   405      \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E\<rbrace>
```
```   406       \<acute>E:=Append_to_free(\<acute>ind,\<acute>E)
```
```   407       FI;;
```
```   408   \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M\<rbrace>
```
```   409    \<acute>ind:=\<acute>ind+1
```
```   410   OD"
```
```   411
```
```   412 lemma Mul_Append:
```
```   413   "\<turnstile> Mul_Append n
```
```   414      \<lbrace>\<acute>Mul_Proper n\<rbrace>"
```
```   415 apply(unfold Mul_Append_def)
```
```   416 apply annhoare
```
```   417 apply(simp_all add: mul_collector_defs Mul_AppendInv_def
```
```   418       Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
```
```   419 apply(force simp add:Blacks_def)
```
```   420 apply(force simp add:Blacks_def)
```
```   421 apply(force simp add:Blacks_def)
```
```   422 apply(force simp add:Graph_defs)
```
```   423 apply force
```
```   424 apply(force simp add:Append_to_free1 Append_to_free2)
```
```   425 apply force
```
```   426 apply force
```
```   427 done
```
```   428
```
```   429 subsubsection \<open>Collector\<close>
```
```   430
```
```   431 definition Mul_Collector :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
```
```   432   "Mul_Collector n \<equiv>
```
```   433 \<lbrace>\<acute>Mul_Proper n\<rbrace>
```
```   434 WHILE True INV \<lbrace>\<acute>Mul_Proper n\<rbrace>
```
```   435 DO
```
```   436 Mul_Blacken_Roots n ;;
```
```   437 \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace>
```
```   438  \<acute>obc:={};;
```
```   439 \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}\<rbrace>
```
```   440  \<acute>bc:=Roots;;
```
```   441 \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots\<rbrace>
```
```   442  \<acute>l:=0;;
```
```   443 \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>l=0\<rbrace>
```
```   444  WHILE \<acute>l<n+1
```
```   445    INV \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and>
```
```   446          (\<acute>Safe \<or> (\<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M) \<and> \<acute>l<n+1)\<rbrace>
```
```   447  DO \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   448       \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M)\<rbrace>
```
```   449     \<acute>obc:=\<acute>bc;;
```
```   450     Mul_Propagate_Black n;;
```
```   451     \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   452       \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   453       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue
```
```   454       \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))\<rbrace>
```
```   455     \<acute>bc:={};;
```
```   456     \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   457       \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   458       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue
```
```   459       \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) \<and> \<acute>bc={}\<rbrace>
```
```   460        \<langle> \<acute>Ma:=\<acute>M,, \<acute>q:=\<acute>Queue \<rangle>;;
```
```   461     Mul_Count n;;
```
```   462     \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   463       \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   464       \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc
```
```   465       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
```
```   466       \<and> \<acute>q<n+1\<rbrace>
```
```   467     IF \<acute>obc=\<acute>bc THEN
```
```   468     \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   469       \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   470       \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc
```
```   471       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
```
```   472       \<and> \<acute>q<n+1 \<and> \<acute>obc=\<acute>bc\<rbrace>
```
```   473     \<acute>l:=\<acute>l+1
```
```   474     ELSE \<lbrace>\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M
```
```   475           \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
```
```   476           \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc
```
```   477           \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>Ma \<or> \<acute>l<\<acute>q \<and> (\<acute>q\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))
```
```   478           \<and> \<acute>q<n+1 \<and> \<acute>obc\<noteq>\<acute>bc\<rbrace>
```
```   479         \<acute>l:=0 FI
```
```   480  OD;;
```
```   481  Mul_Append n
```
```   482 OD"
```
```   483
```
```   484 lemmas mul_modules = Mul_Redirect_Edge_def Mul_Color_Target_def
```
```   485  Mul_Blacken_Roots_def Mul_Propagate_Black_def
```
```   486  Mul_Count_def Mul_Append_def
```
```   487
```
```   488 lemma Mul_Collector:
```
```   489   "\<turnstile> Mul_Collector n
```
```   490   \<lbrace>False\<rbrace>"
```
```   491 apply(unfold Mul_Collector_def)
```
```   492 apply annhoare
```
```   493 apply(simp_all only:pre.simps Mul_Blacken_Roots
```
```   494        Mul_Propagate_Black Mul_Count Mul_Append)
```
```   495 apply(simp_all add:mul_modules)
```
```   496 apply(simp_all add:mul_collector_defs Queue_def)
```
```   497 apply force
```
```   498 apply force
```
```   499 apply force
```
```   500 apply (force simp add: less_Suc_eq_le)
```
```   501 apply force
```
```   502 apply (force dest:subset_antisym)
```
```   503 apply force
```
```   504 apply force
```
```   505 apply force
```
```   506 done
```
```   507
```
```   508 subsection \<open>Interference Freedom\<close>
```
```   509
```
```   510 lemma le_length_filter_update[rule_format]:
```
```   511  "\<forall>i. (\<not>P (list!i) \<or> P j) \<and> i<length list
```
```   512  \<longrightarrow> length(filter P list) \<le> length(filter P (list[i:=j]))"
```
```   513 apply(induct_tac "list")
```
```   514  apply(simp)
```
```   515 apply(clarify)
```
```   516 apply(case_tac i)
```
```   517  apply(simp)
```
```   518 apply(simp)
```
```   519 done
```
```   520
```
```   521 lemma less_length_filter_update [rule_format]:
```
```   522  "\<forall>i. P j \<and> \<not>(P (list!i)) \<and> i<length list
```
```   523  \<longrightarrow> length(filter P list) < length(filter P (list[i:=j]))"
```
```   524 apply(induct_tac "list")
```
```   525  apply(simp)
```
```   526 apply(clarify)
```
```   527 apply(case_tac i)
```
```   528  apply(simp)
```
```   529 apply(simp)
```
```   530 done
```
```   531
```
```   532 lemma Mul_interfree_Blacken_Roots_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk> \<Longrightarrow>
```
```   533   interfree_aux (Some(Mul_Blacken_Roots n),{},Some(Mul_Redirect_Edge j n))"
```
```   534 apply (unfold mul_modules)
```
```   535 apply interfree_aux
```
```   536 apply safe
```
```   537 apply(simp_all add:Graph6 Graph9 Graph12 nth_list_update mul_mutator_defs mul_collector_defs)
```
```   538 done
```
```   539
```
```   540 lemma Mul_interfree_Redirect_Edge_Blacken_Roots: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```   541   interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Blacken_Roots n))"
```
```   542 apply (unfold mul_modules)
```
```   543 apply interfree_aux
```
```   544 apply safe
```
```   545 apply(simp_all add:mul_mutator_defs nth_list_update)
```
```   546 done
```
```   547
```
```   548 lemma Mul_interfree_Blacken_Roots_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```   549   interfree_aux (Some(Mul_Blacken_Roots n),{},Some (Mul_Color_Target j n ))"
```
```   550 apply (unfold mul_modules)
```
```   551 apply interfree_aux
```
```   552 apply safe
```
```   553 apply(simp_all add:mul_mutator_defs mul_collector_defs nth_list_update Graph7 Graph8 Graph9 Graph12)
```
```   554 done
```
```   555
```
```   556 lemma Mul_interfree_Color_Target_Blacken_Roots: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```   557   interfree_aux (Some(Mul_Color_Target j n ),{},Some (Mul_Blacken_Roots n ))"
```
```   558 apply (unfold mul_modules)
```
```   559 apply interfree_aux
```
```   560 apply safe
```
```   561 apply(simp_all add:mul_mutator_defs nth_list_update)
```
```   562 done
```
```   563
```
```   564 lemma Mul_interfree_Propagate_Black_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```   565   interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Redirect_Edge j n ))"
```
```   566 apply (unfold mul_modules)
```
```   567 apply interfree_aux
```
```   568 apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_PBInv_def nth_list_update Graph6)
```
```   569 \<comment> \<open>7 subgoals left\<close>
```
```   570 apply clarify
```
```   571 apply(disjE_tac)
```
```   572   apply(simp_all add:Graph6)
```
```   573  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   574 apply(rule conjI)
```
```   575  apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   576 apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   577 \<comment> \<open>6 subgoals left\<close>
```
```   578 apply clarify
```
```   579 apply(disjE_tac)
```
```   580   apply(simp_all add:Graph6)
```
```   581  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   582 apply(rule conjI)
```
```   583  apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   584 apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   585 \<comment> \<open>5 subgoals left\<close>
```
```   586 apply clarify
```
```   587 apply(disjE_tac)
```
```   588   apply(simp_all add:Graph6)
```
```   589  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   590 apply(rule conjI)
```
```   591  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)
```
```   592 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)
```
```   593 apply(erule conjE)
```
```   594 apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   595  apply(rule conjI)
```
```   596   apply(rule impI,(rule disjI2)+,rule conjI)
```
```   597    apply clarify
```
```   598    apply(case_tac "R (Muts x! j)=i")
```
```   599     apply (force simp add: nth_list_update BtoW_def)
```
```   600    apply (force simp add: nth_list_update)
```
```   601   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   602  apply(rule impI,(rule disjI2)+, erule le_trans)
```
```   603  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   604 apply(rule conjI)
```
```   605  apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
```
```   606  apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
```
```   607 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
```
```   608 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
```
```   609 \<comment> \<open>4 subgoals left\<close>
```
```   610 apply clarify
```
```   611 apply(disjE_tac)
```
```   612   apply(simp_all add:Graph6)
```
```   613  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   614 apply(rule conjI)
```
```   615  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)
```
```   616 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)
```
```   617 apply(erule conjE)
```
```   618 apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   619  apply(rule conjI)
```
```   620   apply(rule impI,(rule disjI2)+,rule conjI)
```
```   621    apply clarify
```
```   622    apply(case_tac "R (Muts x! j)=i")
```
```   623     apply (force simp add: nth_list_update BtoW_def)
```
```   624    apply (force simp add: nth_list_update)
```
```   625   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   626  apply(rule impI,(rule disjI2)+, erule le_trans)
```
```   627  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   628 apply(rule conjI)
```
```   629  apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
```
```   630  apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
```
```   631 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
```
```   632 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
```
```   633 \<comment> \<open>3 subgoals left\<close>
```
```   634 apply clarify
```
```   635 apply(disjE_tac)
```
```   636   apply(simp_all add:Graph6)
```
```   637   apply (rule impI)
```
```   638    apply(rule conjI)
```
```   639     apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   640    apply(case_tac "R (Muts x ! j)= ind x")
```
```   641     apply(simp add:nth_list_update)
```
```   642    apply(simp add:nth_list_update)
```
```   643   apply(case_tac "R (Muts x ! j)= ind x")
```
```   644    apply(simp add:nth_list_update)
```
```   645   apply(simp add:nth_list_update)
```
```   646  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   647   apply(rule conjI)
```
```   648    apply(rule impI)
```
```   649    apply(rule conjI)
```
```   650     apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
```
```   651     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   652    apply(case_tac "R (Muts x ! j)= ind x")
```
```   653     apply(simp add:nth_list_update)
```
```   654    apply(simp add:nth_list_update)
```
```   655   apply(rule impI)
```
```   656   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
```
```   657   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   658  apply(rule conjI)
```
```   659   apply(rule impI)
```
```   660    apply(rule conjI)
```
```   661     apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
```
```   662     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   663    apply(case_tac "R (Muts x ! j)= ind x")
```
```   664     apply(simp add:nth_list_update)
```
```   665    apply(simp add:nth_list_update)
```
```   666   apply(rule impI)
```
```   667   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
```
```   668   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   669  apply(erule conjE)
```
```   670  apply(rule conjI)
```
```   671   apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   672    apply(rule impI,rule conjI,(rule disjI2)+,rule conjI)
```
```   673     apply clarify
```
```   674     apply(case_tac "R (Muts x! j)=i")
```
```   675      apply (force simp add: nth_list_update BtoW_def)
```
```   676     apply (force simp add: nth_list_update)
```
```   677    apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   678   apply(case_tac "R (Muts x ! j)= ind x")
```
```   679    apply(simp add:nth_list_update)
```
```   680   apply(simp add:nth_list_update)
```
```   681  apply(rule impI,rule conjI)
```
```   682   apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
```
```   683   apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
```
```   684  apply(case_tac "R (Muts x! j)=ind x")
```
```   685   apply (force simp add: nth_list_update)
```
```   686  apply (force simp add: nth_list_update)
```
```   687 apply(rule impI, (rule disjI2)+, erule le_trans)
```
```   688 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   689 \<comment> \<open>2 subgoals left\<close>
```
```   690 apply clarify
```
```   691 apply(rule conjI)
```
```   692  apply(disjE_tac)
```
```   693   apply(simp_all add:Mul_Auxk_def Graph6)
```
```   694   apply (rule impI)
```
```   695    apply(rule conjI)
```
```   696     apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   697    apply(case_tac "R (Muts x ! j)= ind x")
```
```   698     apply(simp add:nth_list_update)
```
```   699    apply(simp add:nth_list_update)
```
```   700   apply(case_tac "R (Muts x ! j)= ind x")
```
```   701    apply(simp add:nth_list_update)
```
```   702   apply(simp add:nth_list_update)
```
```   703  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   704   apply(rule impI)
```
```   705   apply(rule conjI)
```
```   706    apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
```
```   707    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   708   apply(case_tac "R (Muts x ! j)= ind x")
```
```   709    apply(simp add:nth_list_update)
```
```   710   apply(simp add:nth_list_update)
```
```   711  apply(rule impI)
```
```   712  apply(rule conjI)
```
```   713   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
```
```   714   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   715  apply(case_tac "R (Muts x ! j)= ind x")
```
```   716   apply(simp add:nth_list_update)
```
```   717  apply(simp add:nth_list_update)
```
```   718 apply(rule impI)
```
```   719 apply(rule conjI)
```
```   720  apply(erule conjE)+
```
```   721  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   722   apply((rule disjI2)+,rule conjI)
```
```   723    apply clarify
```
```   724    apply(case_tac "R (Muts x! j)=i")
```
```   725     apply (force simp add: nth_list_update BtoW_def)
```
```   726    apply (force simp add: nth_list_update)
```
```   727   apply(rule conjI)
```
```   728    apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   729   apply(rule impI)
```
```   730   apply(case_tac "R (Muts x ! j)= ind x")
```
```   731    apply(simp add:nth_list_update BtoW_def)
```
```   732   apply (simp  add:nth_list_update)
```
```   733   apply(rule impI)
```
```   734   apply simp
```
```   735   apply(disjE_tac)
```
```   736    apply(rule disjI1, erule less_le_trans)
```
```   737    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   738   apply force
```
```   739  apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
```
```   740  apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
```
```   741  apply(case_tac "R (Muts x ! j)= ind x")
```
```   742   apply(simp add:nth_list_update)
```
```   743  apply(simp add:nth_list_update)
```
```   744 apply(disjE_tac)
```
```   745 apply simp_all
```
```   746 apply(conjI_tac)
```
```   747  apply(rule impI)
```
```   748  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
```
```   749  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   750 apply(erule conjE)+
```
```   751 apply(rule impI,(rule disjI2)+,rule conjI)
```
```   752  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   753 apply(rule impI)+
```
```   754 apply simp
```
```   755 apply(disjE_tac)
```
```   756  apply(rule disjI1, erule less_le_trans)
```
```   757  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   758 apply force
```
```   759 \<comment> \<open>1 subgoal left\<close>
```
```   760 apply clarify
```
```   761 apply(disjE_tac)
```
```   762   apply(simp_all add:Graph6)
```
```   763  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   764 apply(rule conjI)
```
```   765  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)
```
```   766 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)
```
```   767 apply(erule conjE)
```
```   768 apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   769  apply(rule conjI)
```
```   770   apply(rule impI,(rule disjI2)+,rule conjI)
```
```   771    apply clarify
```
```   772    apply(case_tac "R (Muts x! j)=i")
```
```   773     apply (force simp add: nth_list_update BtoW_def)
```
```   774    apply (force simp add: nth_list_update)
```
```   775   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   776  apply(rule impI,(rule disjI2)+, erule le_trans)
```
```   777  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```   778 apply(rule conjI)
```
```   779  apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
```
```   780  apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
```
```   781 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
```
```   782 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
```
```   783 done
```
```   784
```
```   785 lemma Mul_interfree_Redirect_Edge_Propagate_Black: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```   786   interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Propagate_Black n))"
```
```   787 apply (unfold mul_modules)
```
```   788 apply interfree_aux
```
```   789 apply safe
```
```   790 apply(simp_all add:mul_mutator_defs nth_list_update)
```
```   791 done
```
```   792
```
```   793 lemma Mul_interfree_Propagate_Black_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```   794   interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Color_Target j n ))"
```
```   795 apply (unfold mul_modules)
```
```   796 apply interfree_aux
```
```   797 apply(simp_all add: mul_collector_defs mul_mutator_defs)
```
```   798 \<comment> \<open>7 subgoals left\<close>
```
```   799 apply clarify
```
```   800 apply (simp add:Graph7 Graph8 Graph12)
```
```   801 apply(disjE_tac)
```
```   802   apply(simp add:Graph7 Graph8 Graph12)
```
```   803  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   804   apply(rule disjI2,rule disjI1, erule le_trans)
```
```   805   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   806  apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp)
```
```   807 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
```
```   808 \<comment> \<open>6 subgoals left\<close>
```
```   809 apply clarify
```
```   810 apply (simp add:Graph7 Graph8 Graph12)
```
```   811 apply(disjE_tac)
```
```   812   apply(simp add:Graph7 Graph8 Graph12)
```
```   813  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   814   apply(rule disjI2,rule disjI1, erule le_trans)
```
```   815   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   816  apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp)
```
```   817 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
```
```   818 \<comment> \<open>5 subgoals left\<close>
```
```   819 apply clarify
```
```   820 apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
```
```   821 apply(disjE_tac)
```
```   822    apply(simp add:Graph7 Graph8 Graph12)
```
```   823   apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
```
```   824  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   825   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
```
```   826   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   827  apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
```
```   828 apply(erule conjE)
```
```   829 apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   830  apply((rule disjI2)+)
```
```   831  apply (rule conjI)
```
```   832   apply(simp add:Graph10)
```
```   833  apply(erule le_trans)
```
```   834  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   835 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
```
```   836 \<comment> \<open>4 subgoals left\<close>
```
```   837 apply clarify
```
```   838 apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
```
```   839 apply(disjE_tac)
```
```   840    apply(simp add:Graph7 Graph8 Graph12)
```
```   841   apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
```
```   842  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   843   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
```
```   844   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   845  apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
```
```   846 apply(erule conjE)
```
```   847 apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   848  apply((rule disjI2)+)
```
```   849  apply (rule conjI)
```
```   850   apply(simp add:Graph10)
```
```   851  apply(erule le_trans)
```
```   852  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   853 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
```
```   854 \<comment> \<open>3 subgoals left\<close>
```
```   855 apply clarify
```
```   856 apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
```
```   857 apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   858  apply(simp add:Graph10)
```
```   859  apply(disjE_tac)
```
```   860   apply simp_all
```
```   861   apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
```
```   862   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   863  apply(erule conjE)
```
```   864  apply((rule disjI2)+,erule le_trans)
```
```   865  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   866 apply(rule conjI)
```
```   867  apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11)
```
```   868 apply (force simp add:nth_list_update)
```
```   869 \<comment> \<open>2 subgoals left\<close>
```
```   870 apply clarify
```
```   871 apply(simp add:Mul_Auxk_def Graph7 Graph8 Graph12)
```
```   872 apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   873  apply(simp add:Graph10)
```
```   874  apply(disjE_tac)
```
```   875   apply simp_all
```
```   876   apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
```
```   877   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   878  apply(erule conjE)+
```
```   879  apply((rule disjI2)+,rule conjI, erule le_trans)
```
```   880   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   881  apply((rule impI)+)
```
```   882  apply simp
```
```   883  apply(erule disjE)
```
```   884   apply(rule disjI1, erule less_le_trans)
```
```   885   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   886  apply force
```
```   887 apply(rule conjI)
```
```   888  apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11)
```
```   889 apply (force simp add:nth_list_update)
```
```   890 \<comment> \<open>1 subgoal left\<close>
```
```   891 apply clarify
```
```   892 apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
```
```   893 apply(case_tac "M x!(T (Muts x!j))=Black")
```
```   894  apply(simp add:Graph10)
```
```   895  apply(disjE_tac)
```
```   896   apply simp_all
```
```   897   apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
```
```   898   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   899  apply(erule conjE)
```
```   900  apply((rule disjI2)+,erule le_trans)
```
```   901  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```   902 apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11)
```
```   903 done
```
```   904
```
```   905 lemma Mul_interfree_Color_Target_Propagate_Black: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```   906   interfree_aux (Some(Mul_Color_Target j n),{},Some(Mul_Propagate_Black n ))"
```
```   907 apply (unfold mul_modules)
```
```   908 apply interfree_aux
```
```   909 apply safe
```
```   910 apply(simp_all add:mul_mutator_defs nth_list_update)
```
```   911 done
```
```   912
```
```   913 lemma Mul_interfree_Count_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```   914   interfree_aux (Some(Mul_Count n ),{},Some(Mul_Redirect_Edge j n))"
```
```   915 apply (unfold mul_modules)
```
```   916 apply interfree_aux
```
```   917 \<comment> \<open>9 subgoals left\<close>
```
```   918 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def Graph6)
```
```   919 apply clarify
```
```   920 apply disjE_tac
```
```   921    apply(simp add:Graph6)
```
```   922   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   923  apply(simp add:Graph6)
```
```   924 apply clarify
```
```   925 apply disjE_tac
```
```   926  apply(simp add:Graph6)
```
```   927  apply(rule conjI)
```
```   928   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)
```
```   929  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)
```
```   930 apply(simp add:Graph6)
```
```   931 \<comment> \<open>8 subgoals left\<close>
```
```   932 apply(simp add:mul_mutator_defs nth_list_update)
```
```   933 \<comment> \<open>7 subgoals left\<close>
```
```   934 apply(simp add:mul_mutator_defs mul_collector_defs)
```
```   935 apply clarify
```
```   936 apply disjE_tac
```
```   937    apply(simp add:Graph6)
```
```   938   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   939  apply(simp add:Graph6)
```
```   940 apply clarify
```
```   941 apply disjE_tac
```
```   942  apply(simp add:Graph6)
```
```   943  apply(rule conjI)
```
```   944   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)
```
```   945  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)
```
```   946 apply(simp add:Graph6)
```
```   947 \<comment> \<open>6 subgoals left\<close>
```
```   948 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
```
```   949 apply clarify
```
```   950 apply disjE_tac
```
```   951    apply(simp add:Graph6 Queue_def)
```
```   952   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   953  apply(simp add:Graph6)
```
```   954 apply clarify
```
```   955 apply disjE_tac
```
```   956  apply(simp add:Graph6)
```
```   957  apply(rule conjI)
```
```   958   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)
```
```   959  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)
```
```   960 apply(simp add:Graph6)
```
```   961 \<comment> \<open>5 subgoals left\<close>
```
```   962 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
```
```   963 apply clarify
```
```   964 apply disjE_tac
```
```   965    apply(simp add:Graph6)
```
```   966   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   967  apply(simp add:Graph6)
```
```   968 apply clarify
```
```   969 apply disjE_tac
```
```   970  apply(simp add:Graph6)
```
```   971  apply(rule conjI)
```
```   972   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)
```
```   973  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)
```
```   974 apply(simp add:Graph6)
```
```   975 \<comment> \<open>4 subgoals left\<close>
```
```   976 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
```
```   977 apply clarify
```
```   978 apply disjE_tac
```
```   979    apply(simp add:Graph6)
```
```   980   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   981  apply(simp add:Graph6)
```
```   982 apply clarify
```
```   983 apply disjE_tac
```
```   984  apply(simp add:Graph6)
```
```   985  apply(rule conjI)
```
```   986   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)
```
```   987  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)
```
```   988 apply(simp add:Graph6)
```
```   989 \<comment> \<open>3 subgoals left\<close>
```
```   990 apply(simp add:mul_mutator_defs nth_list_update)
```
```   991 \<comment> \<open>2 subgoals left\<close>
```
```   992 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
```
```   993 apply clarify
```
```   994 apply disjE_tac
```
```   995    apply(simp add:Graph6)
```
```   996   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
```
```   997  apply(simp add:Graph6)
```
```   998 apply clarify
```
```   999 apply disjE_tac
```
```  1000  apply(simp add:Graph6)
```
```  1001  apply(rule conjI)
```
```  1002   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)
```
```  1003  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)
```
```  1004 apply(simp add:Graph6)
```
```  1005 \<comment> \<open>1 subgoal left\<close>
```
```  1006 apply(simp add:mul_mutator_defs nth_list_update)
```
```  1007 done
```
```  1008
```
```  1009 lemma Mul_interfree_Redirect_Edge_Count: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```  1010   interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Count n ))"
```
```  1011 apply (unfold mul_modules)
```
```  1012 apply interfree_aux
```
```  1013 apply safe
```
```  1014 apply(simp_all add:mul_mutator_defs nth_list_update)
```
```  1015 done
```
```  1016
```
```  1017 lemma Mul_interfree_Count_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```  1018   interfree_aux (Some(Mul_Count n ),{},Some(Mul_Color_Target j n))"
```
```  1019 apply (unfold mul_modules)
```
```  1020 apply interfree_aux
```
```  1021 apply(simp_all add:mul_collector_defs mul_mutator_defs Mul_CountInv_def)
```
```  1022 \<comment> \<open>6 subgoals left\<close>
```
```  1023 apply clarify
```
```  1024 apply disjE_tac
```
```  1025   apply (simp add: Graph7 Graph8 Graph12)
```
```  1026  apply (simp add: Graph7 Graph8 Graph12)
```
```  1027 apply clarify
```
```  1028 apply disjE_tac
```
```  1029  apply (simp add: Graph7 Graph8 Graph12)
```
```  1030  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```  1031   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
```
```  1032   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```  1033  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
```
```  1034 apply (simp add: Graph7 Graph8 Graph12)
```
```  1035 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
```
```  1036 \<comment> \<open>5 subgoals left\<close>
```
```  1037 apply clarify
```
```  1038 apply disjE_tac
```
```  1039   apply (simp add: Graph7 Graph8 Graph12)
```
```  1040  apply (simp add: Graph7 Graph8 Graph12)
```
```  1041 apply clarify
```
```  1042 apply disjE_tac
```
```  1043  apply (simp add: Graph7 Graph8 Graph12)
```
```  1044  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```  1045   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
```
```  1046   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```  1047  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
```
```  1048 apply (simp add: Graph7 Graph8 Graph12)
```
```  1049 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
```
```  1050 \<comment> \<open>4 subgoals left\<close>
```
```  1051 apply clarify
```
```  1052 apply disjE_tac
```
```  1053   apply (simp add: Graph7 Graph8 Graph12)
```
```  1054  apply (simp add: Graph7 Graph8 Graph12)
```
```  1055 apply clarify
```
```  1056 apply disjE_tac
```
```  1057  apply (simp add: Graph7 Graph8 Graph12)
```
```  1058  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```  1059   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
```
```  1060   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```  1061  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
```
```  1062 apply (simp add: Graph7 Graph8 Graph12)
```
```  1063 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
```
```  1064 \<comment> \<open>3 subgoals left\<close>
```
```  1065 apply clarify
```
```  1066 apply disjE_tac
```
```  1067   apply (simp add: Graph7 Graph8 Graph12)
```
```  1068  apply (simp add: Graph7 Graph8 Graph12)
```
```  1069 apply clarify
```
```  1070 apply disjE_tac
```
```  1071  apply (simp add: Graph7 Graph8 Graph12)
```
```  1072  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```  1073   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
```
```  1074   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```  1075  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
```
```  1076 apply (simp add: Graph7 Graph8 Graph12)
```
```  1077 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
```
```  1078 \<comment> \<open>2 subgoals left\<close>
```
```  1079 apply clarify
```
```  1080 apply disjE_tac
```
```  1081   apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
```
```  1082  apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
```
```  1083 apply clarify
```
```  1084 apply disjE_tac
```
```  1085  apply (simp add: Graph7 Graph8 Graph12)
```
```  1086  apply(rule conjI)
```
```  1087   apply(case_tac "M x!(T (Muts x!j))=Black")
```
```  1088    apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
```
```  1089    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```  1090   apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
```
```  1091  apply (simp add: nth_list_update)
```
```  1092 apply (simp add: Graph7 Graph8 Graph12)
```
```  1093 apply(rule conjI)
```
```  1094  apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
```
```  1095 apply (simp add: nth_list_update)
```
```  1096 \<comment> \<open>1 subgoal left\<close>
```
```  1097 apply clarify
```
```  1098 apply disjE_tac
```
```  1099   apply (simp add: Graph7 Graph8 Graph12)
```
```  1100  apply (simp add: Graph7 Graph8 Graph12)
```
```  1101 apply clarify
```
```  1102 apply disjE_tac
```
```  1103  apply (simp add: Graph7 Graph8 Graph12)
```
```  1104  apply(case_tac "M x!(T (Muts x!j))=Black")
```
```  1105   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
```
```  1106   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
```
```  1107  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
```
```  1108 apply (simp add: Graph7 Graph8 Graph12)
```
```  1109 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
```
```  1110 done
```
```  1111
```
```  1112 lemma Mul_interfree_Color_Target_Count: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```  1113   interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Count n ))"
```
```  1114 apply (unfold mul_modules)
```
```  1115 apply interfree_aux
```
```  1116 apply safe
```
```  1117 apply(simp_all add:mul_mutator_defs nth_list_update)
```
```  1118 done
```
```  1119
```
```  1120 lemma Mul_interfree_Append_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```  1121   interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
```
```  1122 apply (unfold mul_modules)
```
```  1123 apply interfree_aux
```
```  1124 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```  1125 apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
```
```  1126 apply(erule_tac x=j in allE, force dest:Graph3)+
```
```  1127 done
```
```  1128
```
```  1129 lemma Mul_interfree_Redirect_Edge_Append: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```  1130   interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
```
```  1131 apply (unfold mul_modules)
```
```  1132 apply interfree_aux
```
```  1133 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```  1134 apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def  mul_mutator_defs nth_list_update)
```
```  1135 done
```
```  1136
```
```  1137 lemma Mul_interfree_Append_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```  1138   interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
```
```  1139 apply (unfold mul_modules)
```
```  1140 apply interfree_aux
```
```  1141 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```  1142 apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1
```
```  1143               Graph12 nth_list_update)
```
```  1144 done
```
```  1145
```
```  1146 lemma Mul_interfree_Color_Target_Append: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>
```
```  1147   interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
```
```  1148 apply (unfold mul_modules)
```
```  1149 apply interfree_aux
```
```  1150 apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
```
```  1151 apply(simp_all add: mul_mutator_defs nth_list_update)
```
```  1152 apply(simp add:Mul_AppendInv_def Append_to_free0)
```
```  1153 done
```
```  1154
```
```  1155 subsubsection \<open>Interference freedom Collector-Mutator\<close>
```
```  1156
```
```  1157 lemmas mul_collector_mutator_interfree =
```
```  1158  Mul_interfree_Blacken_Roots_Redirect_Edge Mul_interfree_Blacken_Roots_Color_Target
```
```  1159  Mul_interfree_Propagate_Black_Redirect_Edge Mul_interfree_Propagate_Black_Color_Target
```
```  1160  Mul_interfree_Count_Redirect_Edge Mul_interfree_Count_Color_Target
```
```  1161  Mul_interfree_Append_Redirect_Edge Mul_interfree_Append_Color_Target
```
```  1162  Mul_interfree_Redirect_Edge_Blacken_Roots Mul_interfree_Color_Target_Blacken_Roots
```
```  1163  Mul_interfree_Redirect_Edge_Propagate_Black Mul_interfree_Color_Target_Propagate_Black
```
```  1164  Mul_interfree_Redirect_Edge_Count Mul_interfree_Color_Target_Count
```
```  1165  Mul_interfree_Redirect_Edge_Append Mul_interfree_Color_Target_Append
```
```  1166
```
```  1167 lemma Mul_interfree_Collector_Mutator: "j<n  \<Longrightarrow>
```
```  1168   interfree_aux (Some (Mul_Collector n), {}, Some (Mul_Mutator j n))"
```
```  1169 apply(unfold Mul_Collector_def Mul_Mutator_def)
```
```  1170 apply interfree_aux
```
```  1171 apply(simp_all add:mul_collector_mutator_interfree)
```
```  1172 apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
```
```  1173 apply(tactic  \<open>TRYALL (interfree_aux_tac @{context})\<close>)
```
```  1174 \<comment> \<open>42 subgoals left\<close>
```
```  1175 apply (clarify,simp add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)+
```
```  1176 \<comment> \<open>24 subgoals left\<close>
```
```  1177 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
```
```  1178 \<comment> \<open>14 subgoals left\<close>
```
```  1179 apply(tactic \<open>TRYALL (clarify_tac @{context})\<close>)
```
```  1180 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
```
```  1181 apply(tactic \<open>TRYALL (resolve_tac @{context} [conjI])\<close>)
```
```  1182 apply(tactic \<open>TRYALL (resolve_tac @{context} [impI])\<close>)
```
```  1183 apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
```
```  1184 apply(tactic \<open>TRYALL (eresolve_tac @{context} [conjE])\<close>)
```
```  1185 apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
```
```  1186 apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
```
```  1187 \<comment> \<open>72 subgoals left\<close>
```
```  1188 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
```
```  1189 \<comment> \<open>35 subgoals left\<close>
```
```  1190 apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI1],
```
```  1191     resolve_tac @{context} [subset_trans],
```
```  1192     eresolve_tac @{context} @{thms Graph3},
```
```  1193     force_tac @{context},
```
```  1194     assume_tac @{context}])\<close>)
```
```  1195 \<comment> \<open>28 subgoals left\<close>
```
```  1196 apply(tactic \<open>TRYALL (eresolve_tac @{context} [conjE])\<close>)
```
```  1197 apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
```
```  1198 \<comment> \<open>34 subgoals left\<close>
```
```  1199 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```  1200 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
```
```  1201 apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
```
```  1202 apply(simp_all add:Graph10)
```
```  1203 \<comment> \<open>47 subgoals left\<close>
```
```  1204 apply(tactic \<open>TRYALL(EVERY'[REPEAT o resolve_tac @{context} [disjI2],
```
```  1205     eresolve_tac @{context} @{thms subset_psubset_trans},
```
```  1206     eresolve_tac @{context} @{thms Graph11},
```
```  1207     force_tac @{context}])\<close>)
```
```  1208 \<comment> \<open>41 subgoals left\<close>
```
```  1209 apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
```
```  1210     resolve_tac @{context} [disjI1],
```
```  1211     eresolve_tac @{context} @{thms le_trans},
```
```  1212     force_tac (@{context} addsimps @{thms Queue_def less_Suc_eq_le le_length_filter_update})])\<close>)
```
```  1213 \<comment> \<open>35 subgoals left\<close>
```
```  1214 apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
```
```  1215     resolve_tac @{context} [disjI1],
```
```  1216     eresolve_tac @{context} @{thms psubset_subset_trans},
```
```  1217     resolve_tac @{context} @{thms Graph9},
```
```  1218     force_tac @{context}])\<close>)
```
```  1219 \<comment> \<open>31 subgoals left\<close>
```
```  1220 apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
```
```  1221     resolve_tac @{context} [disjI1],
```
```  1222     eresolve_tac @{context} @{thms subset_psubset_trans},
```
```  1223     eresolve_tac @{context} @{thms Graph11},
```
```  1224     force_tac @{context}])\<close>)
```
```  1225 \<comment> \<open>29 subgoals left\<close>
```
```  1226 apply(tactic \<open>TRYALL(EVERY'[REPEAT o resolve_tac @{context} [disjI2],
```
```  1227     eresolve_tac @{context} @{thms subset_psubset_trans},
```
```  1228     eresolve_tac @{context} @{thms subset_psubset_trans},
```
```  1229     eresolve_tac @{context} @{thms Graph11},
```
```  1230     force_tac @{context}])\<close>)
```
```  1231 \<comment> \<open>25 subgoals left\<close>
```
```  1232 apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
```
```  1233     resolve_tac @{context} [disjI2],
```
```  1234     resolve_tac @{context} [disjI1],
```
```  1235     eresolve_tac @{context} @{thms le_trans},
```
```  1236     force_tac (@{context} addsimps @{thms Queue_def less_Suc_eq_le le_length_filter_update})])\<close>)
```
```  1237 \<comment> \<open>10 subgoals left\<close>
```
```  1238 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)+
```
```  1239 done
```
```  1240
```
```  1241 subsubsection \<open>Interference freedom Mutator-Collector\<close>
```
```  1242
```
```  1243 lemma Mul_interfree_Mutator_Collector: " j < n \<Longrightarrow>
```
```  1244   interfree_aux (Some (Mul_Mutator j n), {}, Some (Mul_Collector n))"
```
```  1245 apply(unfold Mul_Collector_def Mul_Mutator_def)
```
```  1246 apply interfree_aux
```
```  1247 apply(simp_all add:mul_collector_mutator_interfree)
```
```  1248 apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
```
```  1249 apply(tactic  \<open>TRYALL (interfree_aux_tac @{context})\<close>)
```
```  1250 \<comment> \<open>76 subgoals left\<close>
```
```  1251 apply (clarsimp simp add: nth_list_update)+
```
```  1252 \<comment> \<open>56 subgoals left\<close>
```
```  1253 apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
```
```  1254 done
```
```  1255
```
```  1256 subsubsection \<open>The Multi-Mutator Garbage Collection Algorithm\<close>
```
```  1257
```
```  1258 text \<open>The total number of verification conditions is 328\<close>
```
```  1259
```
```  1260 lemma Mul_Gar_Coll:
```
```  1261  "\<parallel>- \<lbrace>\<acute>Mul_Proper n \<and> \<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))\<rbrace>
```
```  1262  COBEGIN
```
```  1263   Mul_Collector n
```
```  1264  \<lbrace>False\<rbrace>
```
```  1265  \<parallel>
```
```  1266  SCHEME  [0\<le> j< n]
```
```  1267   Mul_Mutator j n
```
```  1268  \<lbrace>False\<rbrace>
```
```  1269  COEND
```
```  1270  \<lbrace>False\<rbrace>"
```
```  1271 apply oghoare
```
```  1272 \<comment> \<open>Strengthening the precondition\<close>
```
```  1273 apply(rule Int_greatest)
```
```  1274  apply (case_tac n)
```
```  1275   apply(force simp add: Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
```
```  1276  apply(simp add: Mul_Mutator_def mul_collector_defs mul_mutator_defs nth_append)
```
```  1277  apply force
```
```  1278 apply clarify
```
```  1279 apply(case_tac i)
```
```  1280  apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
```
```  1281 apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt)
```
```  1282 \<comment> \<open>Collector\<close>
```
```  1283 apply(rule Mul_Collector)
```
```  1284 \<comment> \<open>Mutator\<close>
```
```  1285 apply(erule Mul_Mutator)
```
```  1286 \<comment> \<open>Interference freedom\<close>
```
```  1287 apply(simp add:Mul_interfree_Collector_Mutator)
```
```  1288 apply(simp add:Mul_interfree_Mutator_Collector)
```
```  1289 apply(simp add:Mul_interfree_Mutator_Mutator)
```
```  1290 \<comment> \<open>Weakening of the postcondition\<close>
```
```  1291 apply(case_tac n)
```
```  1292  apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
```
```  1293 apply(simp add:Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append)
```
```  1294 done
```
```  1295
```
```  1296 end
```