src/HOL/Hoare_Parallel/Gar_Coll.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62042 6c6ccf573479
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 section \<open>The Single Mutator Case\<close>
     2 
     3 theory Gar_Coll imports Graph OG_Syntax begin
     4 
     5 declare psubsetE [rule del]
     6 
     7 text \<open>Declaration of variables:\<close>
     8 
     9 record gar_coll_state =
    10   M :: nodes
    11   E :: edges
    12   bc :: "nat set"
    13   obc :: "nat set"
    14   Ma :: nodes
    15   ind :: nat
    16   k :: nat
    17   z :: bool
    18 
    19 subsection \<open>The Mutator\<close>
    20 
    21 text \<open>The mutator first redirects an arbitrary edge \<open>R\<close> from
    22 an arbitrary accessible node towards an arbitrary accessible node
    23 \<open>T\<close>.  It then colors the new target \<open>T\<close> black.
    24 
    25 We declare the arbitrarily selected node and edge as constants:\<close>
    26 
    27 consts R :: nat  T :: nat
    28 
    29 text \<open>\noindent The following predicate states, given a list of
    30 nodes \<open>m\<close> and a list of edges \<open>e\<close>, the conditions
    31 under which the selected edge \<open>R\<close> and node \<open>T\<close> are
    32 valid:\<close>
    33 
    34 definition Mut_init :: "gar_coll_state \<Rightarrow> bool" where
    35   "Mut_init \<equiv> \<guillemotleft> T \<in> Reach \<acute>E \<and> R < length \<acute>E \<and> T < length \<acute>M \<guillemotright>"
    36 
    37 text \<open>\noindent For the mutator we
    38 consider two modules, one for each action.  An auxiliary variable
    39 \<open>\<acute>z\<close> is set to false if the mutator has already redirected an
    40 edge but has not yet colored the new target.\<close>
    41 
    42 definition Redirect_Edge :: "gar_coll_state ann_com" where
    43   "Redirect_Edge \<equiv> \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace> \<langle>\<acute>E:=\<acute>E[R:=(fst(\<acute>E!R), T)],, \<acute>z:= (\<not>\<acute>z)\<rangle>"
    44 
    45 definition Color_Target :: "gar_coll_state ann_com" where
    46   "Color_Target \<equiv> \<lbrace>\<acute>Mut_init \<and> \<not>\<acute>z\<rbrace> \<langle>\<acute>M:=\<acute>M[T:=Black],, \<acute>z:= (\<not>\<acute>z)\<rangle>"
    47 
    48 definition Mutator :: "gar_coll_state ann_com" where
    49   "Mutator \<equiv>
    50   \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace>
    51   WHILE True INV \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace>
    52   DO  Redirect_Edge ;; Color_Target  OD"
    53 
    54 subsubsection \<open>Correctness of the mutator\<close>
    55 
    56 lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def
    57 
    58 lemma Redirect_Edge:
    59   "\<turnstile> Redirect_Edge pre(Color_Target)"
    60 apply (unfold mutator_defs)
    61 apply annhoare
    62 apply(simp_all)
    63 apply(force elim:Graph2)
    64 done
    65 
    66 lemma Color_Target:
    67   "\<turnstile> Color_Target \<lbrace>\<acute>Mut_init \<and> \<acute>z\<rbrace>"
    68 apply (unfold mutator_defs)
    69 apply annhoare
    70 apply(simp_all)
    71 done
    72 
    73 lemma Mutator:
    74  "\<turnstile> Mutator \<lbrace>False\<rbrace>"
    75 apply(unfold Mutator_def)
    76 apply annhoare
    77 apply(simp_all add:Redirect_Edge Color_Target)
    78 apply(simp add:mutator_defs)
    79 done
    80 
    81 subsection \<open>The Collector\<close>
    82 
    83 text \<open>\noindent A constant \<open>M_init\<close> is used to give \<open>\<acute>Ma\<close> a
    84 suitable first value, defined as a list of nodes where only the \<open>Roots\<close> are black.\<close>
    85 
    86 consts  M_init :: nodes
    87 
    88 definition Proper_M_init :: "gar_coll_state \<Rightarrow> bool" where
    89   "Proper_M_init \<equiv>  \<guillemotleft> Blacks M_init=Roots \<and> length M_init=length \<acute>M \<guillemotright>"
    90 
    91 definition Proper :: "gar_coll_state \<Rightarrow> bool" where
    92   "Proper \<equiv> \<guillemotleft> Proper_Roots \<acute>M \<and> Proper_Edges(\<acute>M, \<acute>E) \<and> \<acute>Proper_M_init \<guillemotright>"
    93 
    94 definition Safe :: "gar_coll_state \<Rightarrow> bool" where
    95   "Safe \<equiv> \<guillemotleft> Reach \<acute>E \<subseteq> Blacks \<acute>M \<guillemotright>"
    96 
    97 lemmas collector_defs = Proper_M_init_def Proper_def Safe_def
    98 
    99 subsubsection \<open>Blackening the roots\<close>
   100 
   101 definition Blacken_Roots :: " gar_coll_state ann_com" where
   102   "Blacken_Roots \<equiv>
   103   \<lbrace>\<acute>Proper\<rbrace>
   104   \<acute>ind:=0;;
   105   \<lbrace>\<acute>Proper \<and> \<acute>ind=0\<rbrace>
   106   WHILE \<acute>ind<length \<acute>M
   107    INV \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
   108   DO \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
   109    IF \<acute>ind\<in>Roots THEN
   110    \<lbrace>\<acute>Proper \<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>
   111     \<acute>M:=\<acute>M[\<acute>ind:=Black] FI;;
   112    \<lbrace>\<acute>Proper \<and> (\<forall>i<\<acute>ind+1. i \<in> Roots \<longrightarrow> \<acute>M!i=Black) \<and> \<acute>ind<length \<acute>M\<rbrace>
   113     \<acute>ind:=\<acute>ind+1
   114   OD"
   115 
   116 lemma Blacken_Roots:
   117  "\<turnstile> Blacken_Roots \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace>"
   118 apply (unfold Blacken_Roots_def)
   119 apply annhoare
   120 apply(simp_all add:collector_defs Graph_defs)
   121 apply safe
   122 apply(simp_all add:nth_list_update)
   123   apply (erule less_SucE)
   124    apply simp+
   125  apply force
   126 apply force
   127 done
   128 
   129 subsubsection \<open>Propagating black\<close>
   130 
   131 definition PBInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
   132   "PBInv \<equiv> \<guillemotleft> \<lambda>ind. \<acute>obc < Blacks \<acute>M \<or> (\<forall>i <ind. \<not>BtoW (\<acute>E!i, \<acute>M) \<or>
   133    (\<not>\<acute>z \<and> i=R \<and> (snd(\<acute>E!R)) = T \<and> (\<exists>r. ind \<le> r \<and> r < length \<acute>E \<and> BtoW(\<acute>E!r,\<acute>M))))\<guillemotright>"
   134 
   135 definition Propagate_Black_aux :: "gar_coll_state ann_com" where
   136   "Propagate_Black_aux \<equiv>
   137   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M\<rbrace>
   138   \<acute>ind:=0;;
   139   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0\<rbrace>
   140   WHILE \<acute>ind<length \<acute>E
   141    INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   142          \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E\<rbrace>
   143   DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   144        \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace>
   145    IF \<acute>M!(fst (\<acute>E!\<acute>ind)) = Black THEN
   146     \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   147        \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> \<acute>M!fst(\<acute>E!\<acute>ind)=Black\<rbrace>
   148      \<acute>M:=\<acute>M[snd(\<acute>E!\<acute>ind):=Black];;
   149     \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   150        \<and> \<acute>PBInv (\<acute>ind + 1) \<and> \<acute>ind<length \<acute>E\<rbrace>
   151      \<acute>ind:=\<acute>ind+1
   152    FI
   153   OD"
   154 
   155 lemma Propagate_Black_aux:
   156   "\<turnstile>  Propagate_Black_aux
   157   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   158     \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace>"
   159 apply (unfold Propagate_Black_aux_def  PBInv_def collector_defs)
   160 apply annhoare
   161 apply(simp_all add:Graph6 Graph7 Graph8 Graph12)
   162       apply force
   163      apply force
   164     apply force
   165 \<comment>\<open>4 subgoals left\<close>
   166 apply clarify
   167 apply(simp add:Proper_Edges_def Proper_Roots_def Graph6 Graph7 Graph8 Graph12)
   168 apply (erule disjE)
   169  apply(rule disjI1)
   170  apply(erule Graph13)
   171  apply force
   172 apply (case_tac "M x ! snd (E x ! ind x)=Black")
   173  apply (simp add: Graph10 BtoW_def)
   174  apply (rule disjI2)
   175  apply clarify
   176  apply (erule less_SucE)
   177   apply (erule_tac x=i in allE , erule (1) notE impE)
   178   apply simp
   179   apply clarify
   180   apply (drule_tac y = r in le_imp_less_or_eq)
   181   apply (erule disjE)
   182    apply (subgoal_tac "Suc (ind x)\<le>r")
   183     apply fast
   184    apply arith
   185   apply fast
   186  apply fast
   187 apply(rule disjI1)
   188 apply(erule subset_psubset_trans)
   189 apply(erule Graph11)
   190 apply fast
   191 \<comment>\<open>3 subgoals left\<close>
   192 apply force
   193 apply force
   194 \<comment>\<open>last\<close>
   195 apply clarify
   196 apply simp
   197 apply(subgoal_tac "ind x = length (E x)")
   198  apply (simp)
   199  apply(drule Graph1)
   200    apply simp
   201   apply clarify
   202   apply(erule allE, erule impE, assumption)
   203   apply force
   204  apply force
   205 apply arith
   206 done
   207 
   208 subsubsection \<open>Refining propagating black\<close>
   209 
   210 definition Auxk :: "gar_coll_state \<Rightarrow> bool" where
   211   "Auxk \<equiv> \<guillemotleft>\<acute>k<length \<acute>M \<and> (\<acute>M!\<acute>k\<noteq>Black \<or> \<not>BtoW(\<acute>E!\<acute>ind, \<acute>M) \<or>
   212           \<acute>obc<Blacks \<acute>M \<or> (\<not>\<acute>z \<and> \<acute>ind=R \<and> snd(\<acute>E!R)=T
   213           \<and> (\<exists>r. \<acute>ind<r \<and> r<length \<acute>E \<and> BtoW(\<acute>E!r, \<acute>M))))\<guillemotright>"
   214 
   215 definition Propagate_Black :: " gar_coll_state ann_com" where
   216   "Propagate_Black \<equiv>
   217   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M\<rbrace>
   218   \<acute>ind:=0;;
   219   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> \<acute>ind=0\<rbrace>
   220   WHILE \<acute>ind<length \<acute>E
   221    INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   222          \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E\<rbrace>
   223   DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   224        \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace>
   225    IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))=Black THEN
   226     \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   227       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black\<rbrace>
   228      \<acute>k:=(snd(\<acute>E!\<acute>ind));;
   229     \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   230       \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black
   231       \<and> \<acute>Auxk\<rbrace>
   232      \<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],, \<acute>ind:=\<acute>ind+1\<rangle>
   233    ELSE \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   234           \<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E\<rbrace>
   235          \<langle>IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle>
   236    FI
   237   OD"
   238 
   239 lemma Propagate_Black:
   240   "\<turnstile>  Propagate_Black
   241   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   242     \<and> ( \<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace>"
   243 apply (unfold Propagate_Black_def  PBInv_def Auxk_def collector_defs)
   244 apply annhoare
   245 apply(simp_all add: Graph6 Graph7 Graph8 Graph12)
   246        apply force
   247       apply force
   248      apply force
   249 \<comment>\<open>5 subgoals left\<close>
   250 apply clarify
   251 apply(simp add:BtoW_def Proper_Edges_def)
   252 \<comment>\<open>4 subgoals left\<close>
   253 apply clarify
   254 apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
   255 apply (erule disjE)
   256  apply (rule disjI1)
   257  apply (erule psubset_subset_trans)
   258  apply (erule Graph9)
   259 apply (case_tac "M x!k x=Black")
   260  apply (case_tac "M x ! snd (E x ! ind x)=Black")
   261   apply (simp add: Graph10 BtoW_def)
   262   apply (rule disjI2)
   263   apply clarify
   264   apply (erule less_SucE)
   265    apply (erule_tac x=i in allE , erule (1) notE impE)
   266    apply simp
   267    apply clarify
   268    apply (drule_tac y = r in le_imp_less_or_eq)
   269    apply (erule disjE)
   270     apply (subgoal_tac "Suc (ind x)\<le>r")
   271      apply fast
   272     apply arith
   273    apply fast
   274   apply fast
   275  apply (simp add: Graph10 BtoW_def)
   276  apply (erule disjE)
   277   apply (erule disjI1)
   278  apply clarify
   279  apply (erule less_SucE)
   280   apply force
   281  apply simp
   282  apply (subgoal_tac "Suc R\<le>r")
   283   apply fast
   284  apply arith
   285 apply(rule disjI1)
   286 apply(erule subset_psubset_trans)
   287 apply(erule Graph11)
   288 apply fast
   289 \<comment>\<open>2 subgoals left\<close>
   290 apply clarify
   291 apply(simp add:Proper_Edges_def Graph6 Graph7 Graph8 Graph12)
   292 apply (erule disjE)
   293  apply fast
   294 apply clarify
   295 apply (erule less_SucE)
   296  apply (erule_tac x=i in allE , erule (1) notE impE)
   297  apply simp
   298  apply clarify
   299  apply (drule_tac y = r in le_imp_less_or_eq)
   300  apply (erule disjE)
   301   apply (subgoal_tac "Suc (ind x)\<le>r")
   302    apply fast
   303   apply arith
   304  apply (simp add: BtoW_def)
   305 apply (simp add: BtoW_def)
   306 \<comment>\<open>last\<close>
   307 apply clarify
   308 apply simp
   309 apply(subgoal_tac "ind x = length (E x)")
   310  apply (simp)
   311  apply(drule Graph1)
   312    apply simp
   313   apply clarify
   314   apply(erule allE, erule impE, assumption)
   315   apply force
   316  apply force
   317 apply arith
   318 done
   319 
   320 subsubsection \<open>Counting black nodes\<close>
   321 
   322 definition CountInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
   323   "CountInv \<equiv> \<guillemotleft> \<lambda>ind. {i. i<ind \<and> \<acute>Ma!i=Black}\<subseteq>\<acute>bc \<guillemotright>"
   324 
   325 definition Count :: " gar_coll_state ann_com" where
   326   "Count \<equiv>
   327   \<lbrace>\<acute>Proper \<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>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}\<rbrace>
   330   \<acute>ind:=0;;
   331   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
   332     \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   333    \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={}
   334    \<and> \<acute>ind=0\<rbrace>
   335    WHILE \<acute>ind<length \<acute>M
   336      INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
   337            \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   338            \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
   339            \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
   340    DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
   341          \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   342          \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind
   343          \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M\<rbrace>
   344        IF \<acute>M!\<acute>ind=Black
   345           THEN \<lbrace>\<acute>Proper \<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> \<acute>CountInv \<acute>ind
   348                  \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace>
   349           \<acute>bc:=insert \<acute>ind \<acute>bc
   350        FI;;
   351       \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
   352         \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   353         \<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv (\<acute>ind+1)
   354         \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M\<rbrace>
   355       \<acute>ind:=\<acute>ind+1
   356    OD"
   357 
   358 lemma Count:
   359   "\<turnstile> Count
   360   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
   361    \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M
   362    \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace>"
   363 apply(unfold Count_def)
   364 apply annhoare
   365 apply(simp_all add:CountInv_def Graph6 Graph7 Graph8 Graph12 Blacks_def collector_defs)
   366       apply force
   367      apply force
   368     apply force
   369    apply clarify
   370    apply simp
   371    apply(fast elim:less_SucE)
   372   apply clarify
   373   apply simp
   374   apply(fast elim:less_SucE)
   375  apply force
   376 apply force
   377 done
   378 
   379 subsubsection \<open>Appending garbage nodes to the free list\<close>
   380 
   381 axiomatization Append_to_free :: "nat \<times> edges \<Rightarrow> edges"
   382 where
   383   Append_to_free0: "length (Append_to_free (i, e)) = length e" and
   384   Append_to_free1: "Proper_Edges (m, e)
   385                    \<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and
   386   Append_to_free2: "i \<notin> Reach e
   387      \<Longrightarrow> n \<in> Reach (Append_to_free(i, e)) = ( n = i \<or> n \<in> Reach e)"
   388 
   389 definition AppendInv :: "gar_coll_state \<Rightarrow> nat \<Rightarrow> bool" where
   390   "AppendInv \<equiv> \<guillemotleft>\<lambda>ind. \<forall>i<length \<acute>M. ind\<le>i \<longrightarrow> i\<in>Reach \<acute>E \<longrightarrow> \<acute>M!i=Black\<guillemotright>"
   391 
   392 definition Append :: "gar_coll_state ann_com" where
   393    "Append \<equiv>
   394   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe\<rbrace>
   395   \<acute>ind:=0;;
   396   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>Safe \<and> \<acute>ind=0\<rbrace>
   397     WHILE \<acute>ind<length \<acute>M
   398       INV \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>M\<rbrace>
   399     DO \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M\<rbrace>
   400        IF \<acute>M!\<acute>ind=Black THEN
   401           \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace>
   402           \<acute>M:=\<acute>M[\<acute>ind:=White]
   403        ELSE \<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>ind\<notin>Reach \<acute>E\<rbrace>
   404               \<acute>E:=Append_to_free(\<acute>ind,\<acute>E)
   405        FI;;
   406      \<lbrace>\<acute>Proper \<and> \<acute>AppendInv (\<acute>ind+1) \<and> \<acute>ind<length \<acute>M\<rbrace>
   407        \<acute>ind:=\<acute>ind+1
   408     OD"
   409 
   410 lemma Append:
   411   "\<turnstile> Append \<lbrace>\<acute>Proper\<rbrace>"
   412 apply(unfold Append_def AppendInv_def)
   413 apply annhoare
   414 apply(simp_all add:collector_defs Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
   415        apply(force simp:Blacks_def nth_list_update)
   416       apply force
   417      apply force
   418     apply(force simp add:Graph_defs)
   419    apply force
   420   apply clarify
   421   apply simp
   422   apply(rule conjI)
   423    apply (erule Append_to_free1)
   424   apply clarify
   425   apply (drule_tac n = "i" in Append_to_free2)
   426   apply force
   427  apply force
   428 apply force
   429 done
   430 
   431 subsubsection \<open>Correctness of the Collector\<close>
   432 
   433 definition Collector :: " gar_coll_state ann_com" where
   434   "Collector \<equiv>
   435 \<lbrace>\<acute>Proper\<rbrace>
   436  WHILE True INV \<lbrace>\<acute>Proper\<rbrace>
   437  DO
   438   Blacken_Roots;;
   439   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace>
   440    \<acute>obc:={};;
   441   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}\<rbrace>
   442    \<acute>bc:=Roots;;
   443   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots\<rbrace>
   444    \<acute>Ma:=M_init;;
   445   \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>Ma=M_init\<rbrace>
   446    WHILE \<acute>obc\<noteq>\<acute>bc
   447      INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M
   448            \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   449            \<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace>
   450    DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M\<rbrace>
   451        \<acute>obc:=\<acute>bc;;
   452        Propagate_Black;;
   453       \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M
   454         \<and> (\<acute>obc < Blacks \<acute>M \<or> \<acute>Safe)\<rbrace>
   455        \<acute>Ma:=\<acute>M;;
   456       \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma
   457         \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M
   458         \<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace>
   459        \<acute>bc:={};;
   460        Count
   461    OD;;
   462   Append
   463  OD"
   464 
   465 lemma Collector:
   466   "\<turnstile> Collector \<lbrace>False\<rbrace>"
   467 apply(unfold Collector_def)
   468 apply annhoare
   469 apply(simp_all add: Blacken_Roots Propagate_Black Count Append)
   470 apply(simp_all add:Blacken_Roots_def Propagate_Black_def Count_def Append_def collector_defs)
   471    apply (force simp add: Proper_Roots_def)
   472   apply force
   473  apply force
   474 apply clarify
   475 apply (erule disjE)
   476 apply(simp add:psubsetI)
   477  apply(force dest:subset_antisym)
   478 done
   479 
   480 subsection \<open>Interference Freedom\<close>
   481 
   482 lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def
   483                  Propagate_Black_def Count_def Append_def
   484 lemmas Invariants = PBInv_def Auxk_def CountInv_def AppendInv_def
   485 lemmas abbrev = collector_defs mutator_defs Invariants
   486 
   487 lemma interfree_Blacken_Roots_Redirect_Edge:
   488  "interfree_aux (Some Blacken_Roots, {}, Some Redirect_Edge)"
   489 apply (unfold modules)
   490 apply interfree_aux
   491 apply safe
   492 apply (simp_all add:Graph6 Graph12 abbrev)
   493 done
   494 
   495 lemma interfree_Redirect_Edge_Blacken_Roots:
   496   "interfree_aux (Some Redirect_Edge, {}, Some Blacken_Roots)"
   497 apply (unfold modules)
   498 apply interfree_aux
   499 apply safe
   500 apply(simp add:abbrev)+
   501 done
   502 
   503 lemma interfree_Blacken_Roots_Color_Target:
   504   "interfree_aux (Some Blacken_Roots, {}, Some Color_Target)"
   505 apply (unfold modules)
   506 apply interfree_aux
   507 apply safe
   508 apply(simp_all add:Graph7 Graph8 nth_list_update abbrev)
   509 done
   510 
   511 lemma interfree_Color_Target_Blacken_Roots:
   512   "interfree_aux (Some Color_Target, {}, Some Blacken_Roots)"
   513 apply (unfold modules )
   514 apply interfree_aux
   515 apply safe
   516 apply(simp add:abbrev)+
   517 done
   518 
   519 lemma interfree_Propagate_Black_Redirect_Edge:
   520   "interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)"
   521 apply (unfold modules )
   522 apply interfree_aux
   523 \<comment>\<open>11 subgoals left\<close>
   524 apply(clarify, simp add:abbrev Graph6 Graph12)
   525 apply(clarify, simp add:abbrev Graph6 Graph12)
   526 apply(clarify, simp add:abbrev Graph6 Graph12)
   527 apply(clarify, simp add:abbrev Graph6 Graph12)
   528 apply(erule conjE)+
   529 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
   530  apply(erule Graph4)
   531    apply(simp)+
   532   apply (simp add:BtoW_def)
   533  apply (simp add:BtoW_def)
   534 apply(rule conjI)
   535  apply (force simp add:BtoW_def)
   536 apply(erule Graph4)
   537    apply simp+
   538 \<comment>\<open>7 subgoals left\<close>
   539 apply(clarify, simp add:abbrev Graph6 Graph12)
   540 apply(erule conjE)+
   541 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
   542  apply(erule Graph4)
   543    apply(simp)+
   544   apply (simp add:BtoW_def)
   545  apply (simp add:BtoW_def)
   546 apply(rule conjI)
   547  apply (force simp add:BtoW_def)
   548 apply(erule Graph4)
   549    apply simp+
   550 \<comment>\<open>6 subgoals left\<close>
   551 apply(clarify, simp add:abbrev Graph6 Graph12)
   552 apply(erule conjE)+
   553 apply(rule conjI)
   554  apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
   555   apply(erule Graph4)
   556     apply(simp)+
   557    apply (simp add:BtoW_def)
   558   apply (simp add:BtoW_def)
   559  apply(rule conjI)
   560   apply (force simp add:BtoW_def)
   561  apply(erule Graph4)
   562     apply simp+
   563 apply(simp add:BtoW_def nth_list_update)
   564 apply force
   565 \<comment>\<open>5 subgoals left\<close>
   566 apply(clarify, simp add:abbrev Graph6 Graph12)
   567 \<comment>\<open>4 subgoals left\<close>
   568 apply(clarify, simp add:abbrev Graph6 Graph12)
   569 apply(rule conjI)
   570  apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
   571   apply(erule Graph4)
   572     apply(simp)+
   573    apply (simp add:BtoW_def)
   574   apply (simp add:BtoW_def)
   575  apply(rule conjI)
   576   apply (force simp add:BtoW_def)
   577  apply(erule Graph4)
   578     apply simp+
   579 apply(rule conjI)
   580  apply(simp add:nth_list_update)
   581  apply force
   582 apply(rule impI, rule impI, erule disjE, erule disjI1, case_tac "R = (ind x)" ,case_tac "M x ! T = Black")
   583   apply(force simp add:BtoW_def)
   584  apply(case_tac "M x !snd (E x ! ind x)=Black")
   585   apply(rule disjI2)
   586   apply simp
   587   apply (erule Graph5)
   588   apply simp+
   589  apply(force simp add:BtoW_def)
   590 apply(force simp add:BtoW_def)
   591 \<comment>\<open>3 subgoals left\<close>
   592 apply(clarify, simp add:abbrev Graph6 Graph12)
   593 \<comment>\<open>2 subgoals left\<close>
   594 apply(clarify, simp add:abbrev Graph6 Graph12)
   595 apply(erule disjE, erule disjI1, rule disjI2, rule allI, (rule impI)+, case_tac "R=i", rule conjI, erule sym)
   596  apply clarify
   597  apply(erule Graph4)
   598    apply(simp)+
   599   apply (simp add:BtoW_def)
   600  apply (simp add:BtoW_def)
   601 apply(rule conjI)
   602  apply (force simp add:BtoW_def)
   603 apply(erule Graph4)
   604    apply simp+
   605 done
   606 
   607 lemma interfree_Redirect_Edge_Propagate_Black:
   608   "interfree_aux (Some Redirect_Edge, {}, Some Propagate_Black)"
   609 apply (unfold modules )
   610 apply interfree_aux
   611 apply(clarify, simp add:abbrev)+
   612 done
   613 
   614 lemma interfree_Propagate_Black_Color_Target:
   615   "interfree_aux (Some Propagate_Black, {}, Some Color_Target)"
   616 apply (unfold modules )
   617 apply interfree_aux
   618 \<comment>\<open>11 subgoals left\<close>
   619 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)+
   620 apply(erule conjE)+
   621 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
   622       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
   623       erule allE, erule impE, assumption, erule impE, assumption,
   624       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
   625 \<comment>\<open>7 subgoals left\<close>
   626 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
   627 apply(erule conjE)+
   628 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
   629       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
   630       erule allE, erule impE, assumption, erule impE, assumption,
   631       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
   632 \<comment>\<open>6 subgoals left\<close>
   633 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
   634 apply clarify
   635 apply (rule conjI)
   636  apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
   637       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
   638       erule allE, erule impE, assumption, erule impE, assumption,
   639       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
   640 apply(simp add:nth_list_update)
   641 \<comment>\<open>5 subgoals left\<close>
   642 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
   643 \<comment>\<open>4 subgoals left\<close>
   644 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
   645 apply (rule conjI)
   646  apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
   647       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
   648       erule allE, erule impE, assumption, erule impE, assumption,
   649       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
   650 apply(rule conjI)
   651 apply(simp add:nth_list_update)
   652 apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10,
   653       erule subset_psubset_trans, erule Graph11, force)
   654 \<comment>\<open>3 subgoals left\<close>
   655 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
   656 \<comment>\<open>2 subgoals left\<close>
   657 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
   658 apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9,
   659       case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify,
   660       erule allE, erule impE, assumption, erule impE, assumption,
   661       simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force)
   662 \<comment>\<open>3 subgoals left\<close>
   663 apply(simp add:abbrev)
   664 done
   665 
   666 lemma interfree_Color_Target_Propagate_Black:
   667   "interfree_aux (Some Color_Target, {}, Some Propagate_Black)"
   668 apply (unfold modules )
   669 apply interfree_aux
   670 apply(clarify, simp add:abbrev)+
   671 done
   672 
   673 lemma interfree_Count_Redirect_Edge:
   674   "interfree_aux (Some Count, {}, Some Redirect_Edge)"
   675 apply (unfold modules)
   676 apply interfree_aux
   677 \<comment>\<open>9 subgoals left\<close>
   678 apply(simp_all add:abbrev Graph6 Graph12)
   679 \<comment>\<open>6 subgoals left\<close>
   680 apply(clarify, simp add:abbrev Graph6 Graph12,
   681       erule disjE,erule disjI1,rule disjI2,rule subset_trans, erule Graph3,force,force)+
   682 done
   683 
   684 lemma interfree_Redirect_Edge_Count:
   685   "interfree_aux (Some Redirect_Edge, {}, Some Count)"
   686 apply (unfold modules )
   687 apply interfree_aux
   688 apply(clarify,simp add:abbrev)+
   689 apply(simp add:abbrev)
   690 done
   691 
   692 lemma interfree_Count_Color_Target:
   693   "interfree_aux (Some Count, {}, Some Color_Target)"
   694 apply (unfold modules )
   695 apply interfree_aux
   696 \<comment>\<open>9 subgoals left\<close>
   697 apply(simp_all add:abbrev Graph7 Graph8 Graph12)
   698 \<comment>\<open>6 subgoals left\<close>
   699 apply(clarify,simp add:abbrev Graph7 Graph8 Graph12,
   700       erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+
   701 \<comment>\<open>2 subgoals left\<close>
   702 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)
   703 apply(rule conjI)
   704  apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
   705 apply(simp add:nth_list_update)
   706 \<comment>\<open>1 subgoal left\<close>
   707 apply(clarify, simp add:abbrev Graph7 Graph8 Graph12,
   708       erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)
   709 done
   710 
   711 lemma interfree_Color_Target_Count:
   712   "interfree_aux (Some Color_Target, {}, Some Count)"
   713 apply (unfold modules )
   714 apply interfree_aux
   715 apply(clarify, simp add:abbrev)+
   716 apply(simp add:abbrev)
   717 done
   718 
   719 lemma interfree_Append_Redirect_Edge:
   720   "interfree_aux (Some Append, {}, Some Redirect_Edge)"
   721 apply (unfold modules )
   722 apply interfree_aux
   723 apply( simp_all add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12)
   724 apply(clarify, simp add:abbrev Graph6 Append_to_free0 Append_to_free1 Graph12, force dest:Graph3)+
   725 done
   726 
   727 lemma interfree_Redirect_Edge_Append:
   728   "interfree_aux (Some Redirect_Edge, {}, Some Append)"
   729 apply (unfold modules )
   730 apply interfree_aux
   731 apply(clarify, simp add:abbrev Append_to_free0)+
   732 apply (force simp add: Append_to_free2)
   733 apply(clarify, simp add:abbrev Append_to_free0)+
   734 done
   735 
   736 lemma interfree_Append_Color_Target:
   737   "interfree_aux (Some Append, {}, Some Color_Target)"
   738 apply (unfold modules )
   739 apply interfree_aux
   740 apply(clarify, simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)+
   741 apply(simp add:abbrev Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12 nth_list_update)
   742 done
   743 
   744 lemma interfree_Color_Target_Append:
   745   "interfree_aux (Some Color_Target, {}, Some Append)"
   746 apply (unfold modules )
   747 apply interfree_aux
   748 apply(clarify, simp add:abbrev Append_to_free0)+
   749 apply (force simp add: Append_to_free2)
   750 apply(clarify,simp add:abbrev Append_to_free0)+
   751 done
   752 
   753 lemmas collector_mutator_interfree =
   754  interfree_Blacken_Roots_Redirect_Edge interfree_Blacken_Roots_Color_Target
   755  interfree_Propagate_Black_Redirect_Edge interfree_Propagate_Black_Color_Target
   756  interfree_Count_Redirect_Edge interfree_Count_Color_Target
   757  interfree_Append_Redirect_Edge interfree_Append_Color_Target
   758  interfree_Redirect_Edge_Blacken_Roots interfree_Color_Target_Blacken_Roots
   759  interfree_Redirect_Edge_Propagate_Black interfree_Color_Target_Propagate_Black
   760  interfree_Redirect_Edge_Count interfree_Color_Target_Count
   761  interfree_Redirect_Edge_Append interfree_Color_Target_Append
   762 
   763 subsubsection \<open>Interference freedom Collector-Mutator\<close>
   764 
   765 lemma interfree_Collector_Mutator:
   766  "interfree_aux (Some Collector, {}, Some Mutator)"
   767 apply(unfold Collector_def Mutator_def)
   768 apply interfree_aux
   769 apply(simp_all add:collector_mutator_interfree)
   770 apply(unfold modules collector_defs Mut_init_def)
   771 apply(tactic  \<open>TRYALL (interfree_aux_tac @{context})\<close>)
   772 \<comment>\<open>32 subgoals left\<close>
   773 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
   774 \<comment>\<open>20 subgoals left\<close>
   775 apply(tactic\<open>TRYALL (clarify_tac @{context})\<close>)
   776 apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
   777 apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
   778 apply simp_all
   779 apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
   780     resolve_tac @{context} [subset_trans],
   781     eresolve_tac @{context} @{thms Graph3},
   782     force_tac @{context},
   783     assume_tac @{context}])\<close>)
   784 apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
   785     eresolve_tac @{context} [subset_trans],
   786     resolve_tac @{context} @{thms Graph9},
   787     force_tac @{context}])\<close>)
   788 apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI1],
   789     eresolve_tac @{context} @{thms psubset_subset_trans},
   790     resolve_tac @{context} @{thms Graph9},
   791     force_tac @{context}])\<close>)
   792 done
   793 
   794 subsubsection \<open>Interference freedom Mutator-Collector\<close>
   795 
   796 lemma interfree_Mutator_Collector:
   797  "interfree_aux (Some Mutator, {}, Some Collector)"
   798 apply(unfold Collector_def Mutator_def)
   799 apply interfree_aux
   800 apply(simp_all add:collector_mutator_interfree)
   801 apply(unfold modules collector_defs Mut_init_def)
   802 apply(tactic  \<open>TRYALL (interfree_aux_tac @{context})\<close>)
   803 \<comment>\<open>64 subgoals left\<close>
   804 apply(simp_all add:nth_list_update Invariants Append_to_free0)+
   805 apply(tactic\<open>TRYALL (clarify_tac @{context})\<close>)
   806 \<comment>\<open>4 subgoals left\<close>
   807 apply force
   808 apply(simp add:Append_to_free2)
   809 apply force
   810 apply(simp add:Append_to_free2)
   811 done
   812 
   813 subsubsection \<open>The Garbage Collection algorithm\<close>
   814 
   815 text \<open>In total there are 289 verification conditions.\<close>
   816 
   817 lemma Gar_Coll:
   818   "\<parallel>- \<lbrace>\<acute>Proper \<and> \<acute>Mut_init \<and> \<acute>z\<rbrace>
   819   COBEGIN
   820    Collector
   821   \<lbrace>False\<rbrace>
   822  \<parallel>
   823    Mutator
   824   \<lbrace>False\<rbrace>
   825  COEND
   826   \<lbrace>False\<rbrace>"
   827 apply oghoare
   828 apply(force simp add: Mutator_def Collector_def modules)
   829 apply(rule Collector)
   830 apply(rule Mutator)
   831 apply(simp add:interfree_Collector_Mutator)
   832 apply(simp add:interfree_Mutator_Collector)
   833 apply force
   834 done
   835 
   836 end