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