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