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