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