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