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