src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
author haftmann
Mon Mar 01 13:40:23 2010 +0100 (2010-03-01)
changeset 35416 d8d7d1b785af
parent 32960 69916a850301
child 39159 0dec18004e75
permissions -rw-r--r--
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
     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 @{claset}) *})
   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 consts  Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
   384 
   385 axioms
   386   Append_to_free0: "length (Append_to_free (i, e)) = length e"
   387   Append_to_free1: "Proper_Edges (m, e) 
   388                     \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))"
   389   Append_to_free2: "i \<notin> Reach e 
   390            \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
   391 
   392 definition Mul_AppendInv :: "mul_gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
   393   "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>"
   394 
   395 definition Mul_Append :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   396   "Mul_Append n \<equiv> 
   397   .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe}.
   398   \<acute>ind:=0;;
   399   .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0}.
   400   WHILE \<acute>ind<length \<acute>M 
   401     INV .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M}.
   402   DO .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M}.
   403       IF \<acute>M!\<acute>ind=Black THEN 
   404      .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black}. 
   405       \<acute>M:=\<acute>M[\<acute>ind:=White] 
   406       ELSE 
   407      .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E}. 
   408       \<acute>E:=Append_to_free(\<acute>ind,\<acute>E)
   409       FI;;
   410   .{\<acute>Mul_Proper n \<and> \<acute>Mul_AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M}. 
   411    \<acute>ind:=\<acute>ind+1
   412   OD"
   413 
   414 lemma Mul_Append: 
   415   "\<turnstile> Mul_Append n  
   416      .{\<acute>Mul_Proper n}."
   417 apply(unfold Mul_Append_def)
   418 apply annhoare
   419 apply(simp_all add: mul_collector_defs Mul_AppendInv_def 
   420       Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
   421 apply(force simp add:Blacks_def)
   422 apply(force simp add:Blacks_def)
   423 apply(force simp add:Blacks_def)
   424 apply(force simp add:Graph_defs)
   425 apply force
   426 apply(force simp add:Append_to_free1 Append_to_free2)
   427 apply force
   428 apply force
   429 done
   430 
   431 subsubsection {* Collector *}
   432 
   433 definition Mul_Collector :: "nat \<Rightarrow>  mul_gar_coll_state ann_com" where
   434   "Mul_Collector n \<equiv>
   435 .{\<acute>Mul_Proper n}.  
   436 WHILE True INV .{\<acute>Mul_Proper n}. 
   437 DO  
   438 Mul_Blacken_Roots n ;; 
   439 .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M}.  
   440  \<acute>obc:={};; 
   441 .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}}.  
   442  \<acute>bc:=Roots;; 
   443 .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots}. 
   444  \<acute>l:=0;; 
   445 .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>l=0}. 
   446  WHILE \<acute>l<n+1  
   447    INV .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and>  
   448          (\<acute>Safe \<or> (\<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M) \<and> \<acute>l<n+1)}. 
   449  DO .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
   450       \<and> (\<acute>Safe \<or> \<acute>l\<le>\<acute>Queue \<or> \<acute>bc\<subset>Blacks \<acute>M)}.
   451     \<acute>obc:=\<acute>bc;;
   452     Mul_Propagate_Black n;; 
   453     .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
   454       \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
   455       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
   456       \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M))}. 
   457     \<acute>bc:={};;
   458     .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
   459       \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
   460       \<and> (\<acute>Safe \<or> \<acute>obc\<subset>Blacks \<acute>M \<or> \<acute>l<\<acute>Queue 
   461       \<and> (\<acute>l\<le>\<acute>Queue \<or> \<acute>obc\<subset>Blacks \<acute>M)) \<and> \<acute>bc={}}. 
   462        \<langle> \<acute>Ma:=\<acute>M,, \<acute>q:=\<acute>Queue \<rangle>;;
   463     Mul_Count n;; 
   464     .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
   465       \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
   466       \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
   467       \<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)) 
   468       \<and> \<acute>q<n+1}. 
   469     IF \<acute>obc=\<acute>bc THEN
   470     .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
   471       \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
   472       \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
   473       \<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)) 
   474       \<and> \<acute>q<n+1 \<and> \<acute>obc=\<acute>bc}.  
   475     \<acute>l:=\<acute>l+1  
   476     ELSE .{\<acute>Mul_Proper n \<and> Roots\<subseteq>Blacks \<acute>M 
   477           \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M 
   478           \<and> length \<acute>Ma=length \<acute>M \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc 
   479           \<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)) 
   480           \<and> \<acute>q<n+1 \<and> \<acute>obc\<noteq>\<acute>bc}.  
   481         \<acute>l:=0 FI 
   482  OD;; 
   483  Mul_Append n  
   484 OD"
   485 
   486 lemmas mul_modules = Mul_Redirect_Edge_def Mul_Color_Target_def 
   487  Mul_Blacken_Roots_def Mul_Propagate_Black_def 
   488  Mul_Count_def Mul_Append_def
   489 
   490 lemma Mul_Collector:
   491   "\<turnstile> Mul_Collector n 
   492   .{False}."
   493 apply(unfold Mul_Collector_def)
   494 apply annhoare
   495 apply(simp_all only:pre.simps Mul_Blacken_Roots 
   496        Mul_Propagate_Black Mul_Count Mul_Append)
   497 apply(simp_all add:mul_modules)
   498 apply(simp_all add:mul_collector_defs Queue_def)
   499 apply force
   500 apply force
   501 apply force
   502 apply (force simp add: less_Suc_eq_le)
   503 apply force
   504 apply (force dest:subset_antisym)
   505 apply force
   506 apply force
   507 apply force
   508 done
   509 
   510 subsection {* Interference Freedom *}
   511 
   512 lemma le_length_filter_update[rule_format]: 
   513  "\<forall>i. (\<not>P (list!i) \<or> P j) \<and> i<length list 
   514  \<longrightarrow> length(filter P list) \<le> length(filter P (list[i:=j]))"
   515 apply(induct_tac "list")
   516  apply(simp)
   517 apply(clarify)
   518 apply(case_tac i)
   519  apply(simp)
   520 apply(simp)
   521 done
   522 
   523 lemma less_length_filter_update [rule_format]: 
   524  "\<forall>i. P j \<and> \<not>(P (list!i)) \<and> i<length list 
   525  \<longrightarrow> length(filter P list) < length(filter P (list[i:=j]))"
   526 apply(induct_tac "list")
   527  apply(simp)
   528 apply(clarify)
   529 apply(case_tac i)
   530  apply(simp)
   531 apply(simp)
   532 done
   533 
   534 lemma Mul_interfree_Blacken_Roots_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk> \<Longrightarrow>  
   535   interfree_aux (Some(Mul_Blacken_Roots n),{},Some(Mul_Redirect_Edge j n))"
   536 apply (unfold mul_modules)
   537 apply interfree_aux
   538 apply safe
   539 apply(simp_all add:Graph6 Graph9 Graph12 nth_list_update mul_mutator_defs mul_collector_defs)
   540 done
   541 
   542 lemma Mul_interfree_Redirect_Edge_Blacken_Roots: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow> 
   543   interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Blacken_Roots n))"
   544 apply (unfold mul_modules)
   545 apply interfree_aux
   546 apply safe
   547 apply(simp_all add:mul_mutator_defs nth_list_update)
   548 done
   549 
   550 lemma Mul_interfree_Blacken_Roots_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
   551   interfree_aux (Some(Mul_Blacken_Roots n),{},Some (Mul_Color_Target j n ))"
   552 apply (unfold mul_modules)
   553 apply interfree_aux
   554 apply safe
   555 apply(simp_all add:mul_mutator_defs mul_collector_defs nth_list_update Graph7 Graph8 Graph9 Graph12)
   556 done
   557 
   558 lemma Mul_interfree_Color_Target_Blacken_Roots: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
   559   interfree_aux (Some(Mul_Color_Target j n ),{},Some (Mul_Blacken_Roots n ))"
   560 apply (unfold mul_modules)
   561 apply interfree_aux
   562 apply safe
   563 apply(simp_all add:mul_mutator_defs nth_list_update)
   564 done
   565 
   566 lemma Mul_interfree_Propagate_Black_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
   567   interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Redirect_Edge j n ))"
   568 apply (unfold mul_modules)
   569 apply interfree_aux
   570 apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_PBInv_def nth_list_update Graph6)
   571 --{* 7 subgoals left *}
   572 apply clarify
   573 apply(disjE_tac)
   574   apply(simp_all add:Graph6)
   575  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   576 apply(rule conjI)
   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 apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   579 --{* 6 subgoals left *}
   580 apply clarify
   581 apply(disjE_tac)
   582   apply(simp_all add:Graph6)
   583  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   584 apply(rule conjI)
   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 apply(rule impI,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   587 --{* 5 subgoals left *}
   588 apply clarify
   589 apply(disjE_tac)
   590   apply(simp_all add:Graph6)
   591  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   592 apply(rule conjI)
   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(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)
   595 apply(erule conjE)
   596 apply(case_tac "M x!(T (Muts x!j))=Black")
   597  apply(rule conjI)
   598   apply(rule impI,(rule disjI2)+,rule conjI)
   599    apply clarify
   600    apply(case_tac "R (Muts x! j)=i")
   601     apply (force simp add: nth_list_update BtoW_def)
   602    apply (force simp add: nth_list_update)
   603   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   604  apply(rule impI,(rule disjI2)+, erule le_trans)
   605  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   606 apply(rule conjI)
   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 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
   610 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
   611 --{* 4 subgoals left *}
   612 apply clarify
   613 apply(disjE_tac)
   614   apply(simp_all add:Graph6)
   615  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   616 apply(rule conjI)
   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(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)
   619 apply(erule conjE)
   620 apply(case_tac "M x!(T (Muts x!j))=Black")
   621  apply(rule conjI)
   622   apply(rule impI,(rule disjI2)+,rule conjI)
   623    apply clarify
   624    apply(case_tac "R (Muts x! j)=i")
   625     apply (force simp add: nth_list_update BtoW_def)
   626    apply (force simp add: nth_list_update)
   627   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   628  apply(rule impI,(rule disjI2)+, erule le_trans)
   629  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   630 apply(rule conjI)
   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 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
   634 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
   635 --{* 3 subgoals left *}
   636 apply clarify
   637 apply(disjE_tac)
   638   apply(simp_all add:Graph6)
   639   apply (rule impI)
   640    apply(rule conjI)
   641     apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   642    apply(case_tac "R (Muts x ! j)= ind x")
   643     apply(simp add:nth_list_update)
   644    apply(simp add:nth_list_update)
   645   apply(case_tac "R (Muts x ! j)= ind x")
   646    apply(simp add:nth_list_update)
   647   apply(simp add:nth_list_update)
   648  apply(case_tac "M x!(T (Muts x!j))=Black")
   649   apply(rule conjI)
   650    apply(rule impI)
   651    apply(rule conjI)
   652     apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   653     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   654    apply(case_tac "R (Muts x ! j)= ind x")
   655     apply(simp add:nth_list_update)
   656    apply(simp add:nth_list_update)
   657   apply(rule impI)
   658   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   659   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   660  apply(rule conjI)
   661   apply(rule impI)
   662    apply(rule conjI)
   663     apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   664     apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   665    apply(case_tac "R (Muts x ! j)= ind x")
   666     apply(simp add:nth_list_update)
   667    apply(simp add:nth_list_update)
   668   apply(rule impI)
   669   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   670   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   671  apply(erule conjE)
   672  apply(rule conjI)
   673   apply(case_tac "M x!(T (Muts x!j))=Black")
   674    apply(rule impI,rule conjI,(rule disjI2)+,rule conjI)
   675     apply clarify
   676     apply(case_tac "R (Muts x! j)=i")
   677      apply (force simp add: nth_list_update BtoW_def)
   678     apply (force simp add: nth_list_update)
   679    apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   680   apply(case_tac "R (Muts x ! j)= ind x")
   681    apply(simp add:nth_list_update)
   682   apply(simp add:nth_list_update)
   683  apply(rule impI,rule conjI)
   684   apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
   685   apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
   686  apply(case_tac "R (Muts x! j)=ind x")
   687   apply (force simp add: nth_list_update)
   688  apply (force simp add: nth_list_update)
   689 apply(rule impI, (rule disjI2)+, erule le_trans)
   690 apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   691 --{* 2 subgoals left *}
   692 apply clarify
   693 apply(rule conjI)
   694  apply(disjE_tac)
   695   apply(simp_all add:Mul_Auxk_def Graph6)
   696   apply (rule impI)
   697    apply(rule conjI)
   698     apply(rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   699    apply(case_tac "R (Muts x ! j)= ind x")
   700     apply(simp add:nth_list_update)
   701    apply(simp add:nth_list_update)
   702   apply(case_tac "R (Muts x ! j)= ind x")
   703    apply(simp add:nth_list_update)
   704   apply(simp add:nth_list_update)
   705  apply(case_tac "M x!(T (Muts x!j))=Black")
   706   apply(rule impI)
   707   apply(rule conjI)
   708    apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   709    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   710   apply(case_tac "R (Muts x ! j)= ind x")
   711    apply(simp add:nth_list_update)
   712   apply(simp add:nth_list_update)
   713  apply(rule impI)
   714  apply(rule conjI)
   715   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   716   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   717  apply(case_tac "R (Muts x ! j)= ind x")
   718   apply(simp add:nth_list_update)
   719  apply(simp add:nth_list_update)
   720 apply(rule impI)
   721 apply(rule conjI)
   722  apply(erule conjE)+
   723  apply(case_tac "M x!(T (Muts x!j))=Black")
   724   apply((rule disjI2)+,rule conjI)
   725    apply clarify
   726    apply(case_tac "R (Muts x! j)=i")
   727     apply (force simp add: nth_list_update BtoW_def)
   728    apply (force simp add: nth_list_update)
   729   apply(rule conjI)
   730    apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   731   apply(rule impI)
   732   apply(case_tac "R (Muts x ! j)= ind x")
   733    apply(simp add:nth_list_update BtoW_def)
   734   apply (simp  add:nth_list_update)
   735   apply(rule impI)
   736   apply simp
   737   apply(disjE_tac)
   738    apply(rule disjI1, erule less_le_trans)
   739    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   740   apply force
   741  apply(rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
   742  apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
   743  apply(case_tac "R (Muts x ! j)= ind x")
   744   apply(simp add:nth_list_update)
   745  apply(simp add:nth_list_update)
   746 apply(disjE_tac) 
   747 apply simp_all
   748 apply(conjI_tac)
   749  apply(rule impI)
   750  apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   751  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   752 apply(erule conjE)+
   753 apply(rule impI,(rule disjI2)+,rule conjI)
   754  apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   755 apply(rule impI)+
   756 apply simp
   757 apply(disjE_tac)
   758  apply(rule disjI1, erule less_le_trans)
   759  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   760 apply force
   761 --{* 1 subgoal left *} 
   762 apply clarify
   763 apply(disjE_tac)
   764   apply(simp_all add:Graph6)
   765  apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   766 apply(rule conjI)
   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(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)
   769 apply(erule conjE)
   770 apply(case_tac "M x!(T (Muts x!j))=Black")
   771  apply(rule conjI)
   772   apply(rule impI,(rule disjI2)+,rule conjI)
   773    apply clarify
   774    apply(case_tac "R (Muts x! j)=i")
   775     apply (force simp add: nth_list_update BtoW_def)
   776    apply (force simp add: nth_list_update)
   777   apply(erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   778  apply(rule impI,(rule disjI2)+, erule le_trans)
   779  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   780 apply(rule conjI)
   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 apply(rule impI,rule disjI2,rule disjI2,rule disjI1, erule le_less_trans)
   784 apply(force simp add:Queue_def less_Suc_eq_le less_length_filter_update)
   785 done
   786 
   787 lemma Mul_interfree_Redirect_Edge_Propagate_Black: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
   788   interfree_aux (Some(Mul_Redirect_Edge j n ),{},Some (Mul_Propagate_Black n))"
   789 apply (unfold mul_modules)
   790 apply interfree_aux
   791 apply safe
   792 apply(simp_all add:mul_mutator_defs nth_list_update)
   793 done
   794 
   795 lemma Mul_interfree_Propagate_Black_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
   796   interfree_aux (Some(Mul_Propagate_Black n),{},Some (Mul_Color_Target j n ))"
   797 apply (unfold mul_modules)
   798 apply interfree_aux
   799 apply(simp_all add: mul_collector_defs mul_mutator_defs)
   800 --{* 7 subgoals left *}
   801 apply clarify
   802 apply (simp add:Graph7 Graph8 Graph12)
   803 apply(disjE_tac)
   804   apply(simp add:Graph7 Graph8 Graph12)
   805  apply(case_tac "M x!(T (Muts x!j))=Black")
   806   apply(rule disjI2,rule disjI1, erule le_trans)
   807   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   808  apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) 
   809 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
   810 --{* 6 subgoals left *}
   811 apply clarify
   812 apply (simp add:Graph7 Graph8 Graph12)
   813 apply(disjE_tac)
   814   apply(simp add:Graph7 Graph8 Graph12)
   815  apply(case_tac "M x!(T (Muts x!j))=Black")
   816   apply(rule disjI2,rule disjI1, erule le_trans)
   817   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   818  apply((rule disjI2)+,erule subset_psubset_trans, erule Graph11, simp) 
   819 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
   820 --{* 5 subgoals left *}
   821 apply clarify
   822 apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
   823 apply(disjE_tac)
   824    apply(simp add:Graph7 Graph8 Graph12) 
   825   apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
   826  apply(case_tac "M x!(T (Muts x!j))=Black")
   827   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   828   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   829  apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
   830 apply(erule conjE)
   831 apply(case_tac "M x!(T (Muts x!j))=Black")
   832  apply((rule disjI2)+)
   833  apply (rule conjI)
   834   apply(simp add:Graph10)
   835  apply(erule le_trans)
   836  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   837 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) 
   838 --{* 4 subgoals left *}
   839 apply clarify
   840 apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
   841 apply(disjE_tac)
   842    apply(simp add:Graph7 Graph8 Graph12)
   843   apply(rule disjI2,rule disjI1, erule psubset_subset_trans,simp add:Graph9)
   844  apply(case_tac "M x!(T (Muts x!j))=Black")
   845   apply(rule disjI2,rule disjI2,rule disjI1, erule less_le_trans)
   846   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   847  apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp)
   848 apply(erule conjE)
   849 apply(case_tac "M x!(T (Muts x!j))=Black")
   850  apply((rule disjI2)+)
   851  apply (rule conjI)
   852   apply(simp add:Graph10)
   853  apply(erule le_trans)
   854  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   855 apply(rule disjI2,rule disjI1,erule subset_psubset_trans, erule Graph11, simp) 
   856 --{* 3 subgoals left *}
   857 apply clarify
   858 apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
   859 apply(case_tac "M x!(T (Muts x!j))=Black")
   860  apply(simp add:Graph10)
   861  apply(disjE_tac)
   862   apply simp_all
   863   apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
   864   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   865  apply(erule conjE)
   866  apply((rule disjI2)+,erule le_trans)
   867  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   868 apply(rule conjI)
   869  apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
   870 apply (force simp add:nth_list_update)
   871 --{* 2 subgoals left *}
   872 apply clarify 
   873 apply(simp add:Mul_Auxk_def Graph7 Graph8 Graph12)
   874 apply(case_tac "M x!(T (Muts x!j))=Black")
   875  apply(simp add:Graph10)
   876  apply(disjE_tac)
   877   apply simp_all
   878   apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
   879   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   880  apply(erule conjE)+
   881  apply((rule disjI2)+,rule conjI, erule le_trans)
   882   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   883  apply((rule impI)+)
   884  apply simp
   885  apply(erule disjE)
   886   apply(rule disjI1, erule less_le_trans) 
   887   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   888  apply force
   889 apply(rule conjI)
   890  apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
   891 apply (force simp add:nth_list_update)
   892 --{* 1 subgoal left *}
   893 apply clarify
   894 apply (simp add:mul_collector_defs Mul_PBInv_def Graph7 Graph8 Graph12)
   895 apply(case_tac "M x!(T (Muts x!j))=Black")
   896  apply(simp add:Graph10)
   897  apply(disjE_tac)
   898   apply simp_all
   899   apply(rule disjI2, rule disjI2, rule disjI1,erule less_le_trans)
   900   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   901  apply(erule conjE)
   902  apply((rule disjI2)+,erule le_trans)
   903  apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
   904 apply(rule disjI2,rule disjI1, erule subset_psubset_trans,simp add:Graph11) 
   905 done
   906 
   907 lemma Mul_interfree_Color_Target_Propagate_Black: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
   908   interfree_aux (Some(Mul_Color_Target j n),{},Some(Mul_Propagate_Black n ))"
   909 apply (unfold mul_modules)
   910 apply interfree_aux
   911 apply safe
   912 apply(simp_all add:mul_mutator_defs nth_list_update)
   913 done
   914 
   915 lemma Mul_interfree_Count_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
   916   interfree_aux (Some(Mul_Count n ),{},Some(Mul_Redirect_Edge j n))"
   917 apply (unfold mul_modules)
   918 apply interfree_aux
   919 --{* 9 subgoals left *}
   920 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def Graph6)
   921 apply clarify
   922 apply disjE_tac
   923    apply(simp add:Graph6)
   924   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   925  apply(simp add:Graph6)
   926 apply clarify
   927 apply disjE_tac
   928  apply(simp add:Graph6)
   929  apply(rule conjI)
   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(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   932 apply(simp add:Graph6)
   933 --{* 8 subgoals left *}
   934 apply(simp add:mul_mutator_defs nth_list_update)
   935 --{* 7 subgoals left *}
   936 apply(simp add:mul_mutator_defs mul_collector_defs)
   937 apply clarify
   938 apply disjE_tac
   939    apply(simp add:Graph6)
   940   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   941  apply(simp add:Graph6)
   942 apply clarify
   943 apply disjE_tac
   944  apply(simp add:Graph6)
   945  apply(rule conjI)
   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(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   948 apply(simp add:Graph6)
   949 --{* 6 subgoals left *}
   950 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
   951 apply clarify
   952 apply disjE_tac
   953    apply(simp add:Graph6 Queue_def)
   954   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   955  apply(simp add:Graph6)
   956 apply clarify
   957 apply disjE_tac
   958  apply(simp add:Graph6)
   959  apply(rule conjI)
   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(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   962 apply(simp add:Graph6)
   963 --{* 5 subgoals left *}
   964 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
   965 apply clarify
   966 apply disjE_tac
   967    apply(simp add:Graph6)
   968   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   969  apply(simp add:Graph6)
   970 apply clarify
   971 apply disjE_tac
   972  apply(simp add:Graph6)
   973  apply(rule conjI)
   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(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   976 apply(simp add:Graph6)
   977 --{* 4 subgoals left *}
   978 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
   979 apply clarify
   980 apply disjE_tac
   981    apply(simp add:Graph6)
   982   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   983  apply(simp add:Graph6)
   984 apply clarify
   985 apply disjE_tac
   986  apply(simp add:Graph6)
   987  apply(rule conjI)
   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(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
   990 apply(simp add:Graph6)
   991 --{* 3 subgoals left *}
   992 apply(simp add:mul_mutator_defs nth_list_update)
   993 --{* 2 subgoals left *}
   994 apply(simp add:mul_mutator_defs mul_collector_defs Mul_CountInv_def)
   995 apply clarify
   996 apply disjE_tac
   997    apply(simp add:Graph6)
   998   apply(rule impI,rule disjI1,rule subset_trans,erule Graph3,simp,simp)
   999  apply(simp add:Graph6)
  1000 apply clarify
  1001 apply disjE_tac
  1002  apply(simp add:Graph6)
  1003  apply(rule conjI)
  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(rule impI,rule disjI2,rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
  1006 apply(simp add:Graph6)
  1007 --{* 1 subgoal left *}
  1008 apply(simp add:mul_mutator_defs nth_list_update)
  1009 done
  1010 
  1011 lemma Mul_interfree_Redirect_Edge_Count: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
  1012   interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Count n ))"
  1013 apply (unfold mul_modules)
  1014 apply interfree_aux
  1015 apply safe
  1016 apply(simp_all add:mul_mutator_defs nth_list_update)
  1017 done
  1018 
  1019 lemma Mul_interfree_Count_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
  1020   interfree_aux (Some(Mul_Count n ),{},Some(Mul_Color_Target j n))"
  1021 apply (unfold mul_modules)
  1022 apply interfree_aux
  1023 apply(simp_all add:mul_collector_defs mul_mutator_defs Mul_CountInv_def)
  1024 --{* 6 subgoals left *}
  1025 apply clarify
  1026 apply disjE_tac
  1027   apply (simp add: Graph7 Graph8 Graph12)
  1028  apply (simp add: Graph7 Graph8 Graph12)
  1029 apply clarify
  1030 apply disjE_tac
  1031  apply (simp add: Graph7 Graph8 Graph12)
  1032  apply(case_tac "M x!(T (Muts x!j))=Black")
  1033   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  1034   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
  1035  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
  1036 apply (simp add: Graph7 Graph8 Graph12)
  1037 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
  1038 --{* 5 subgoals left *}
  1039 apply clarify
  1040 apply disjE_tac
  1041   apply (simp add: Graph7 Graph8 Graph12)
  1042  apply (simp add: Graph7 Graph8 Graph12)
  1043 apply clarify
  1044 apply disjE_tac
  1045  apply (simp add: Graph7 Graph8 Graph12)
  1046  apply(case_tac "M x!(T (Muts x!j))=Black")
  1047   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  1048   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
  1049  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
  1050 apply (simp add: Graph7 Graph8 Graph12)
  1051 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
  1052 --{* 4 subgoals left *}
  1053 apply clarify
  1054 apply disjE_tac
  1055   apply (simp add: Graph7 Graph8 Graph12)
  1056  apply (simp add: Graph7 Graph8 Graph12)
  1057 apply clarify
  1058 apply disjE_tac
  1059  apply (simp add: Graph7 Graph8 Graph12)
  1060  apply(case_tac "M x!(T (Muts x!j))=Black")
  1061   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  1062   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
  1063  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
  1064 apply (simp add: Graph7 Graph8 Graph12)
  1065 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
  1066 --{* 3 subgoals left *}
  1067 apply clarify
  1068 apply disjE_tac
  1069   apply (simp add: Graph7 Graph8 Graph12)
  1070  apply (simp add: Graph7 Graph8 Graph12)
  1071 apply clarify
  1072 apply disjE_tac
  1073  apply (simp add: Graph7 Graph8 Graph12)
  1074  apply(case_tac "M x!(T (Muts x!j))=Black")
  1075   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  1076   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
  1077  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
  1078 apply (simp add: Graph7 Graph8 Graph12)
  1079 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
  1080 --{* 2 subgoals left *}
  1081 apply clarify
  1082 apply disjE_tac
  1083   apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
  1084  apply (simp add: Graph7 Graph8 Graph12 nth_list_update)
  1085 apply clarify
  1086 apply disjE_tac
  1087  apply (simp add: Graph7 Graph8 Graph12)
  1088  apply(rule conjI)
  1089   apply(case_tac "M x!(T (Muts x!j))=Black")
  1090    apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  1091    apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
  1092   apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
  1093  apply (simp add: nth_list_update)
  1094 apply (simp add: Graph7 Graph8 Graph12)
  1095 apply(rule conjI)
  1096  apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
  1097 apply (simp add: nth_list_update)
  1098 --{* 1 subgoal left *}
  1099 apply clarify
  1100 apply disjE_tac
  1101   apply (simp add: Graph7 Graph8 Graph12)
  1102  apply (simp add: Graph7 Graph8 Graph12)
  1103 apply clarify
  1104 apply disjE_tac
  1105  apply (simp add: Graph7 Graph8 Graph12)
  1106  apply(case_tac "M x!(T (Muts x!j))=Black")
  1107   apply(rule disjI2,rule disjI2, rule disjI1, erule le_trans)
  1108   apply(force simp add:Queue_def less_Suc_eq_le le_length_filter_update Graph10)
  1109  apply((rule disjI2)+,(erule subset_psubset_trans)+, simp add: Graph11)
  1110 apply (simp add: Graph7 Graph8 Graph12)
  1111 apply((rule disjI2)+,erule psubset_subset_trans, simp add: Graph9)
  1112 done
  1113 
  1114 lemma Mul_interfree_Color_Target_Count: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
  1115   interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Count n ))"
  1116 apply (unfold mul_modules)
  1117 apply interfree_aux
  1118 apply safe
  1119 apply(simp_all add:mul_mutator_defs nth_list_update)
  1120 done
  1121 
  1122 lemma Mul_interfree_Append_Redirect_Edge: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
  1123   interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
  1124 apply (unfold mul_modules)
  1125 apply interfree_aux
  1126 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
  1127 apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
  1128 apply(erule_tac x=j in allE, force dest:Graph3)+
  1129 done
  1130 
  1131 lemma Mul_interfree_Redirect_Edge_Append: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
  1132   interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
  1133 apply (unfold mul_modules)
  1134 apply interfree_aux
  1135 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
  1136 apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def  mul_mutator_defs nth_list_update)
  1137 done
  1138 
  1139 lemma Mul_interfree_Append_Color_Target: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
  1140   interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
  1141 apply (unfold mul_modules)
  1142 apply interfree_aux
  1143 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
  1144 apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1 
  1145               Graph12 nth_list_update)
  1146 done
  1147 
  1148 lemma Mul_interfree_Color_Target_Append: "\<lbrakk>0\<le>j; j<n\<rbrakk>\<Longrightarrow>  
  1149   interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
  1150 apply (unfold mul_modules)
  1151 apply interfree_aux
  1152 apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
  1153 apply(simp_all add: mul_mutator_defs nth_list_update)
  1154 apply(simp add:Mul_AppendInv_def Append_to_free0)
  1155 done
  1156 
  1157 subsubsection {* Interference freedom Collector-Mutator *}
  1158 
  1159 lemmas mul_collector_mutator_interfree =  
  1160  Mul_interfree_Blacken_Roots_Redirect_Edge Mul_interfree_Blacken_Roots_Color_Target 
  1161  Mul_interfree_Propagate_Black_Redirect_Edge Mul_interfree_Propagate_Black_Color_Target  
  1162  Mul_interfree_Count_Redirect_Edge Mul_interfree_Count_Color_Target 
  1163  Mul_interfree_Append_Redirect_Edge Mul_interfree_Append_Color_Target 
  1164  Mul_interfree_Redirect_Edge_Blacken_Roots Mul_interfree_Color_Target_Blacken_Roots 
  1165  Mul_interfree_Redirect_Edge_Propagate_Black Mul_interfree_Color_Target_Propagate_Black  
  1166  Mul_interfree_Redirect_Edge_Count Mul_interfree_Color_Target_Count 
  1167  Mul_interfree_Redirect_Edge_Append Mul_interfree_Color_Target_Append
  1168 
  1169 lemma Mul_interfree_Collector_Mutator: "j<n  \<Longrightarrow> 
  1170   interfree_aux (Some (Mul_Collector n), {}, Some (Mul_Mutator j n))"
  1171 apply(unfold Mul_Collector_def Mul_Mutator_def)
  1172 apply interfree_aux
  1173 apply(simp_all add:mul_collector_mutator_interfree)
  1174 apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
  1175 apply(tactic  {* TRYALL (interfree_aux_tac) *})
  1176 --{* 42 subgoals left *}
  1177 apply (clarify,simp add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)+
  1178 --{* 24 subgoals left *}
  1179 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
  1180 --{* 14 subgoals left *}
  1181 apply(tactic {* TRYALL (clarify_tac @{claset}) *})
  1182 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
  1183 apply(tactic {* TRYALL (rtac conjI) *})
  1184 apply(tactic {* TRYALL (rtac impI) *})
  1185 apply(tactic {* TRYALL (etac disjE) *})
  1186 apply(tactic {* TRYALL (etac conjE) *})
  1187 apply(tactic {* TRYALL (etac disjE) *})
  1188 apply(tactic {* TRYALL (etac disjE) *})
  1189 --{* 72 subgoals left *}
  1190 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
  1191 --{* 35 subgoals left *}
  1192 apply(tactic {* TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{clasimpset}, assume_tac]) *})
  1193 --{* 28 subgoals left *}
  1194 apply(tactic {* TRYALL (etac conjE) *})
  1195 apply(tactic {* TRYALL (etac disjE) *})
  1196 --{* 34 subgoals left *}
  1197 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
  1198 apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update)
  1199 apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
  1200 apply(simp_all add:Graph10)
  1201 --{* 47 subgoals left *}
  1202 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
  1203 --{* 41 subgoals left *}
  1204 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
  1205 --{* 35 subgoals left *}
  1206 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *})
  1207 --{* 31 subgoals left *}
  1208 apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
  1209 --{* 29 subgoals left *}
  1210 apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
  1211 --{* 25 subgoals left *}
  1212 apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *})
  1213 --{* 10 subgoals left *}
  1214 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)+
  1215 done
  1216 
  1217 subsubsection {* Interference freedom Mutator-Collector *}
  1218 
  1219 lemma Mul_interfree_Mutator_Collector: " j < n \<Longrightarrow> 
  1220   interfree_aux (Some (Mul_Mutator j n), {}, Some (Mul_Collector n))"
  1221 apply(unfold Mul_Collector_def Mul_Mutator_def)
  1222 apply interfree_aux
  1223 apply(simp_all add:mul_collector_mutator_interfree)
  1224 apply(unfold mul_modules mul_collector_defs mul_mutator_defs)
  1225 apply(tactic  {* TRYALL (interfree_aux_tac) *})
  1226 --{* 76 subgoals left *}
  1227 apply (clarsimp simp add: nth_list_update)+
  1228 --{* 56 subgoals left *}
  1229 apply (clarsimp simp add: Mul_AppendInv_def Append_to_free0 nth_list_update)+
  1230 done
  1231 
  1232 subsubsection {* The Multi-Mutator Garbage Collection Algorithm *}
  1233 
  1234 text {* The total number of verification conditions is 328 *}
  1235 
  1236 lemma Mul_Gar_Coll: 
  1237  "\<parallel>- .{\<acute>Mul_Proper n \<and> \<acute>Mul_mut_init n \<and> (\<forall>i<n. Z (\<acute>Muts!i))}.  
  1238  COBEGIN  
  1239   Mul_Collector n
  1240  .{False}.
  1241  \<parallel>  
  1242  SCHEME  [0\<le> j< n]
  1243   Mul_Mutator j n
  1244  .{False}.  
  1245  COEND  
  1246  .{False}."
  1247 apply oghoare
  1248 --{* Strengthening the precondition *}
  1249 apply(rule Int_greatest)
  1250  apply (case_tac n)
  1251   apply(force simp add: Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
  1252  apply(simp add: Mul_Mutator_def mul_collector_defs mul_mutator_defs nth_append)
  1253  apply force
  1254 apply clarify
  1255 apply(case_tac i)
  1256  apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
  1257 apply(simp add: Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append nth_map_upt)
  1258 --{* Collector *}
  1259 apply(rule Mul_Collector)
  1260 --{* Mutator *}
  1261 apply(erule Mul_Mutator)
  1262 --{* Interference freedom *}
  1263 apply(simp add:Mul_interfree_Collector_Mutator)
  1264 apply(simp add:Mul_interfree_Mutator_Collector)
  1265 apply(simp add:Mul_interfree_Mutator_Mutator)
  1266 --{* Weakening of the postcondition *}
  1267 apply(case_tac n)
  1268  apply(simp add:Mul_Collector_def mul_mutator_defs mul_collector_defs nth_append)
  1269 apply(simp add:Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append)
  1270 done
  1271 
  1272 end