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