author | wenzelm |
Sat, 18 Jul 2015 20:54:56 +0200 | |
changeset 60754 | 02924903a6fd |
parent 59189 | ad8e0a789af6 |
child 62042 | 6c6ccf573479 |
permissions | -rw-r--r-- |
59189 | 1 |
section \<open>The Single Mutator Case\<close> |
13020 | 2 |
|
16417 | 3 |
theory Gar_Coll imports Graph OG_Syntax begin |
13020 | 4 |
|
13624 | 5 |
declare psubsetE [rule del] |
6 |
||
59189 | 7 |
text \<open>Declaration of variables:\<close> |
13020 | 8 |
|
9 |
record gar_coll_state = |
|
10 |
M :: nodes |
|
11 |
E :: edges |
|
12 |
bc :: "nat set" |
|
13 |
obc :: "nat set" |
|
14 |
Ma :: nodes |
|
59189 | 15 |
ind :: nat |
13020 | 16 |
k :: nat |
17 |
z :: bool |
|
18 |
||
59189 | 19 |
subsection \<open>The Mutator\<close> |
13020 | 20 |
|
59189 | 21 |
text \<open>The mutator first redirects an arbitrary edge @{text "R"} from |
13020 | 22 |
an arbitrary accessible node towards an arbitrary accessible node |
59189 | 23 |
@{text "T"}. It then colors the new target @{text "T"} black. |
13020 | 24 |
|
59189 | 25 |
We declare the arbitrarily selected node and edge as constants:\<close> |
13020 | 26 |
|
27 |
consts R :: nat T :: nat |
|
28 |
||
59189 | 29 |
text \<open>\noindent The following predicate states, given a list of |
13020 | 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 |
|
59189 | 32 |
valid:\<close> |
13020 | 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 |
||
59189 | 37 |
text \<open>\noindent For the mutator we |
13020 | 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 |
|
59189 | 40 |
edge but has not yet colored the new target.\<close> |
13020 | 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> |
59189 | 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 |
||
59189 | 54 |
subsubsection \<open>Correctness of the mutator\<close> |
13020 | 55 |
|
56 |
lemmas mutator_defs = Mut_init_def Redirect_Edge_def Color_Target_def |
|
57 |
||
59189 | 58 |
lemma Redirect_Edge: |
13020 | 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 |
||
59189 | 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 |
||
59189 | 81 |
subsection \<open>The Collector\<close> |
13020 | 82 |
|
59189 | 83 |
text \<open>\noindent A constant @{text "M_init"} is used to give @{text "\<acute>Ma"} a |
13020 | 84 |
suitable first value, defined as a list of nodes where only the @{text |
59189 | 85 |
"Roots"} are black.\<close> |
13020 | 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>" |
59189 | 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 |
||
59189 | 100 |
subsubsection \<open>Blackening the roots\<close> |
13020 | 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 |
59189 | 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> |
59189 | 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> |
|
59189 | 110 |
IF \<acute>ind\<in>Roots THEN |
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> |
59189 | 114 |
\<acute>ind:=\<acute>ind+1 |
13020 | 115 |
OD" |
116 |
||
59189 | 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 |
||
59189 | 130 |
subsubsection \<open>Propagating black\<close> |
13020 | 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;; |
59189 | 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> |
141 |
WHILE \<acute>ind<length \<acute>E |
|
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 |
|
53241 | 143 |
\<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E\<rbrace> |
59189 | 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> |
|
146 |
IF \<acute>M!(fst (\<acute>E!\<acute>ind)) = Black THEN |
|
147 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
53241 | 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];; |
59189 | 150 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
53241 | 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 |
||
59189 | 156 |
lemma Propagate_Black_aux: |
13020 | 157 |
"\<turnstile> Propagate_Black_aux |
59189 | 158 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
53241 | 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 |
|
59189 | 166 |
--\<open>4 subgoals left\<close> |
13020 | 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 |
|
59189 | 192 |
--\<open>3 subgoals left\<close> |
13020 | 193 |
apply force |
194 |
apply force |
|
59189 | 195 |
--\<open>last\<close> |
13020 | 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 |
||
59189 | 209 |
subsubsection \<open>Refining propagating black\<close> |
13020 | 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 |
59189 | 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 |
|
13020 | 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> |
59189 | 221 |
WHILE \<acute>ind<length \<acute>E |
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 |
|
53241 | 223 |
\<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind\<le>length \<acute>E\<rbrace> |
59189 | 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> |
|
226 |
IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))=Black THEN |
|
227 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
53241 | 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));; |
59189 | 230 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
231 |
\<and> \<acute>PBInv \<acute>ind \<and> \<acute>ind<length \<acute>E \<and> (\<acute>M!fst(\<acute>E!\<acute>ind))=Black |
|
53241 | 232 |
\<and> \<acute>Auxk\<rbrace> |
13020 | 233 |
\<langle>\<acute>M:=\<acute>M[\<acute>k:=Black],, \<acute>ind:=\<acute>ind+1\<rangle> |
59189 | 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> |
|
236 |
\<langle>IF (\<acute>M!(fst (\<acute>E!\<acute>ind)))\<noteq>Black THEN \<acute>ind:=\<acute>ind+1 FI\<rangle> |
|
13020 | 237 |
FI |
238 |
OD" |
|
239 |
||
59189 | 240 |
lemma Propagate_Black: |
13020 | 241 |
"\<turnstile> Propagate_Black |
59189 | 242 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
53241 | 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 |
|
59189 | 250 |
--\<open>5 subgoals left\<close> |
13020 | 251 |
apply clarify |
252 |
apply(simp add:BtoW_def Proper_Edges_def) |
|
59189 | 253 |
--\<open>4 subgoals left\<close> |
13020 | 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 |
|
59189 | 290 |
--\<open>2 subgoals left\<close> |
13020 | 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) |
|
59189 | 307 |
--\<open>last\<close> |
13020 | 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 |
|
59189 | 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 |
||
59189 | 321 |
subsubsection \<open>Counting black nodes\<close> |
13020 | 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> |
59189 | 328 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
329 |
\<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
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;; |
59189 | 332 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
333 |
\<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
334 |
\<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>bc={} |
|
53241 | 335 |
\<and> \<acute>ind=0\<rbrace> |
59189 | 336 |
WHILE \<acute>ind<length \<acute>M |
337 |
INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
338 |
\<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
13020 | 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> |
59189 | 341 |
DO \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
342 |
\<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
343 |
\<and> length \<acute>Ma=length \<acute>M \<and> \<acute>CountInv \<acute>ind |
|
344 |
\<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe) \<and> \<acute>ind<length \<acute>M\<rbrace> |
|
345 |
IF \<acute>M!\<acute>ind=Black |
|
346 |
THEN \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
347 |
\<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
13020 | 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;; |
|
59189 | 352 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
353 |
\<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
13020 | 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 |
||
59189 | 359 |
lemma Count: |
360 |
"\<turnstile> Count |
|
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 |
||
59189 | 380 |
subsubsection \<open>Appending garbage nodes to the free list\<close> |
13020 | 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 |
|
59189 | 385 |
Append_to_free1: "Proper_Edges (m, e) |
45827 | 386 |
\<Longrightarrow> Proper_Edges (m, Append_to_free(i, e))" and |
59189 | 387 |
Append_to_free2: "i \<notin> Reach e |
13020 | 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> |
59189 | 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> |
|
59189 | 401 |
IF \<acute>M!\<acute>ind=Black THEN |
402 |
\<lbrace>\<acute>Proper \<and> \<acute>AppendInv \<acute>ind \<and> \<acute>ind<length \<acute>M \<and> \<acute>M!\<acute>ind=Black\<rbrace> |
|
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;; |
|
59189 | 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 |
||
59189 | 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 |
||
59189 | 432 |
subsubsection \<open>Correctness of the Collector\<close> |
13020 | 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> |
59189 | 436 |
\<lbrace>\<acute>Proper\<rbrace> |
437 |
WHILE True INV \<lbrace>\<acute>Proper\<rbrace> |
|
438 |
DO |
|
439 |
Blacken_Roots;; |
|
440 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M\<rbrace> |
|
441 |
\<acute>obc:={};; |
|
442 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={}\<rbrace> |
|
443 |
\<acute>bc:=Roots;; |
|
444 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots\<rbrace> |
|
445 |
\<acute>Ma:=M_init;; |
|
446 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc={} \<and> \<acute>bc=Roots \<and> \<acute>Ma=M_init\<rbrace> |
|
447 |
WHILE \<acute>obc\<noteq>\<acute>bc |
|
448 |
INV \<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M |
|
449 |
\<and> \<acute>obc\<subseteq>Blacks \<acute>Ma \<and> Blacks \<acute>Ma\<subseteq>\<acute>bc \<and> \<acute>bc\<subseteq>Blacks \<acute>M |
|
450 |
\<and> length \<acute>Ma=length \<acute>M \<and> (\<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace> |
|
53241 | 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;; |
59189 | 453 |
Propagate_Black;; |
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;; |
59189 | 457 |
\<lbrace>\<acute>Proper \<and> Roots\<subseteq>Blacks \<acute>M \<and> \<acute>obc\<subseteq>Blacks \<acute>Ma |
458 |
\<and> Blacks \<acute>Ma\<subseteq>Blacks \<acute>M \<and> \<acute>bc\<subseteq>Blacks \<acute>M \<and> length \<acute>Ma=length \<acute>M |
|
53241 | 459 |
\<and> ( \<acute>obc < Blacks \<acute>Ma \<or> \<acute>Safe)\<rbrace> |
13020 | 460 |
\<acute>bc:={};; |
59189 | 461 |
Count |
462 |
OD;; |
|
463 |
Append |
|
13020 | 464 |
OD" |
465 |
||
59189 | 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 |
||
59189 | 481 |
subsection \<open>Interference Freedom\<close> |
13020 | 482 |
|
59189 | 483 |
lemmas modules = Redirect_Edge_def Color_Target_def Blacken_Roots_def |
13020 | 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 |
||
59189 | 488 |
lemma interfree_Blacken_Roots_Redirect_Edge: |
13020 | 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 |
||
59189 | 496 |
lemma interfree_Redirect_Edge_Blacken_Roots: |
13020 | 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 |
||
59189 | 504 |
lemma interfree_Blacken_Roots_Color_Target: |
13020 | 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 |
||
59189 | 512 |
lemma interfree_Color_Target_Blacken_Roots: |
13020 | 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 |
||
59189 | 520 |
lemma interfree_Propagate_Black_Redirect_Edge: |
13020 | 521 |
"interfree_aux (Some Propagate_Black, {}, Some Redirect_Edge)" |
522 |
apply (unfold modules ) |
|
523 |
apply interfree_aux |
|
59189 | 524 |
--\<open>11 subgoals left\<close> |
13020 | 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) |
|
59189 | 531 |
apply(erule Graph4) |
13020 | 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+ |
|
59189 | 539 |
--\<open>7 subgoals left\<close> |
13020 | 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) |
|
59189 | 543 |
apply(erule Graph4) |
13020 | 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+ |
|
59189 | 551 |
--\<open>6 subgoals left\<close> |
13020 | 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) |
|
59189 | 556 |
apply(erule Graph4) |
13020 | 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+ |
|
59189 | 564 |
apply(simp add:BtoW_def nth_list_update) |
13020 | 565 |
apply force |
59189 | 566 |
--\<open>5 subgoals left\<close> |
13020 | 567 |
apply(clarify, simp add:abbrev Graph6 Graph12) |
59189 | 568 |
--\<open>4 subgoals left\<close> |
13020 | 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) |
|
59189 | 572 |
apply(erule Graph4) |
13020 | 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) |
|
59189 | 592 |
--\<open>3 subgoals left\<close> |
13020 | 593 |
apply(clarify, simp add:abbrev Graph6 Graph12) |
59189 | 594 |
--\<open>2 subgoals left\<close> |
13020 | 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 |
|
59189 | 598 |
apply(erule Graph4) |
13020 | 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 |
||
59189 | 608 |
lemma interfree_Redirect_Edge_Propagate_Black: |
13020 | 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 |
||
59189 | 615 |
lemma interfree_Propagate_Black_Color_Target: |
13020 | 616 |
"interfree_aux (Some Propagate_Black, {}, Some Color_Target)" |
617 |
apply (unfold modules ) |
|
618 |
apply interfree_aux |
|
59189 | 619 |
--\<open>11 subgoals left\<close> |
13020 | 620 |
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12)+ |
621 |
apply(erule conjE)+ |
|
59189 | 622 |
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
13020 | 623 |
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
59189 | 624 |
erule allE, erule impE, assumption, erule impE, assumption, |
625 |
simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
626 |
--\<open>7 subgoals left\<close> |
|
13020 | 627 |
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
628 |
apply(erule conjE)+ |
|
59189 | 629 |
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
13020 | 630 |
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
59189 | 631 |
erule allE, erule impE, assumption, erule impE, assumption, |
632 |
simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
633 |
--\<open>6 subgoals left\<close> |
|
13020 | 634 |
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
635 |
apply clarify |
|
636 |
apply (rule conjI) |
|
59189 | 637 |
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
13020 | 638 |
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
59189 | 639 |
erule allE, erule impE, assumption, erule impE, assumption, |
640 |
simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
13020 | 641 |
apply(simp add:nth_list_update) |
59189 | 642 |
--\<open>5 subgoals left\<close> |
13020 | 643 |
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
59189 | 644 |
--\<open>4 subgoals left\<close> |
13020 | 645 |
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
646 |
apply (rule conjI) |
|
59189 | 647 |
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
13020 | 648 |
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
59189 | 649 |
erule allE, erule impE, assumption, erule impE, assumption, |
650 |
simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
13020 | 651 |
apply(rule conjI) |
652 |
apply(simp add:nth_list_update) |
|
59189 | 653 |
apply(rule impI,rule impI, case_tac "M x!T=Black",rotate_tac -1, force simp add: BtoW_def Graph10, |
13020 | 654 |
erule subset_psubset_trans, erule Graph11, force) |
59189 | 655 |
--\<open>3 subgoals left\<close> |
13020 | 656 |
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
59189 | 657 |
--\<open>2 subgoals left\<close> |
13020 | 658 |
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
59189 | 659 |
apply(erule disjE,rule disjI1,erule psubset_subset_trans,erule Graph9, |
13020 | 660 |
case_tac "M x!T=Black", rule disjI2,rotate_tac -1, simp add: Graph10, clarify, |
59189 | 661 |
erule allE, erule impE, assumption, erule impE, assumption, |
662 |
simp add:BtoW_def, rule disjI1, erule subset_psubset_trans, erule Graph11, force) |
|
663 |
--\<open>3 subgoals left\<close> |
|
13020 | 664 |
apply(simp add:abbrev) |
665 |
done |
|
666 |
||
59189 | 667 |
lemma interfree_Color_Target_Propagate_Black: |
13020 | 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 |
||
59189 | 674 |
lemma interfree_Count_Redirect_Edge: |
13020 | 675 |
"interfree_aux (Some Count, {}, Some Redirect_Edge)" |
676 |
apply (unfold modules) |
|
677 |
apply interfree_aux |
|
59189 | 678 |
--\<open>9 subgoals left\<close> |
13020 | 679 |
apply(simp_all add:abbrev Graph6 Graph12) |
59189 | 680 |
--\<open>6 subgoals left\<close> |
13020 | 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 |
||
59189 | 685 |
lemma interfree_Redirect_Edge_Count: |
13020 | 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 |
||
59189 | 693 |
lemma interfree_Count_Color_Target: |
13020 | 694 |
"interfree_aux (Some Count, {}, Some Color_Target)" |
695 |
apply (unfold modules ) |
|
696 |
apply interfree_aux |
|
59189 | 697 |
--\<open>9 subgoals left\<close> |
13020 | 698 |
apply(simp_all add:abbrev Graph7 Graph8 Graph12) |
59189 | 699 |
--\<open>6 subgoals left\<close> |
13020 | 700 |
apply(clarify,simp add:abbrev Graph7 Graph8 Graph12, |
701 |
erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9)+ |
|
59189 | 702 |
--\<open>2 subgoals left\<close> |
13020 | 703 |
apply(clarify, simp add:abbrev Graph7 Graph8 Graph12) |
704 |
apply(rule conjI) |
|
59189 | 705 |
apply(erule disjE, erule disjI1, rule disjI2,erule subset_trans, erule Graph9) |
13020 | 706 |
apply(simp add:nth_list_update) |
59189 | 707 |
--\<open>1 subgoal left\<close> |
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 |
||
59189 | 712 |
lemma interfree_Color_Target_Count: |
13020 | 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 |
||
59189 | 720 |
lemma interfree_Append_Redirect_Edge: |
13020 | 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 |
||
59189 | 728 |
lemma interfree_Redirect_Edge_Append: |
13020 | 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 |
||
59189 | 737 |
lemma interfree_Append_Color_Target: |
13020 | 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 |
||
59189 | 745 |
lemma interfree_Color_Target_Append: |
13020 | 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 |
||
59189 | 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 |
|
13020 | 762 |
interfree_Redirect_Edge_Append interfree_Color_Target_Append |
763 |
||
59189 | 764 |
subsubsection \<open>Interference freedom Collector-Mutator\<close> |
13020 | 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) |
59189 | 772 |
apply(tactic \<open>TRYALL (interfree_aux_tac @{context})\<close>) |
773 |
--\<open>32 subgoals left\<close> |
|
13020 | 774 |
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
59189 | 775 |
--\<open>20 subgoals left\<close> |
776 |
apply(tactic\<open>TRYALL (clarify_tac @{context})\<close>) |
|
13020 | 777 |
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) |
60754 | 778 |
apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>) |
13020 | 779 |
apply simp_all |
60754 | 780 |
apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2], |
781 |
resolve_tac @{context} [subset_trans], |
|
782 |
eresolve_tac @{context} @{thms Graph3}, |
|
783 |
force_tac @{context}, |
|
784 |
assume_tac @{context}])\<close>) |
|
785 |
apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2], |
|
786 |
eresolve_tac @{context} [subset_trans], |
|
787 |
resolve_tac @{context} @{thms Graph9}, |
|
788 |
force_tac @{context}])\<close>) |
|
789 |
apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI1], |
|
790 |
eresolve_tac @{context} @{thms psubset_subset_trans}, |
|
791 |
resolve_tac @{context} @{thms Graph9}, |
|
792 |
force_tac @{context}])\<close>) |
|
13020 | 793 |
done |
794 |
||
59189 | 795 |
subsubsection \<open>Interference freedom Mutator-Collector\<close> |
13020 | 796 |
|
797 |
lemma interfree_Mutator_Collector: |
|
798 |
"interfree_aux (Some Mutator, {}, Some Collector)" |
|
799 |
apply(unfold Collector_def Mutator_def) |
|
800 |
apply interfree_aux |
|
801 |
apply(simp_all add:collector_mutator_interfree) |
|
52597
a8a81453833d
more precise fact declarations -- fewer warnings;
wenzelm
parents:
51717
diff
changeset
|
802 |
apply(unfold modules collector_defs Mut_init_def) |
59189 | 803 |
apply(tactic \<open>TRYALL (interfree_aux_tac @{context})\<close>) |
804 |
--\<open>64 subgoals left\<close> |
|
13020 | 805 |
apply(simp_all add:nth_list_update Invariants Append_to_free0)+ |
59189 | 806 |
apply(tactic\<open>TRYALL (clarify_tac @{context})\<close>) |
807 |
--\<open>4 subgoals left\<close> |
|
13020 | 808 |
apply force |
809 |
apply(simp add:Append_to_free2) |
|
810 |
apply force |
|
811 |
apply(simp add:Append_to_free2) |
|
812 |
done |
|
813 |
||
59189 | 814 |
subsubsection \<open>The Garbage Collection algorithm\<close> |
13020 | 815 |
|
59189 | 816 |
text \<open>In total there are 289 verification conditions.\<close> |
13020 | 817 |
|
59189 | 818 |
lemma Gar_Coll: |
819 |
"\<parallel>- \<lbrace>\<acute>Proper \<and> \<acute>Mut_init \<and> \<acute>z\<rbrace> |
|
820 |
COBEGIN |
|
13020 | 821 |
Collector |
53241 | 822 |
\<lbrace>False\<rbrace> |
59189 | 823 |
\<parallel> |
13020 | 824 |
Mutator |
59189 | 825 |
\<lbrace>False\<rbrace> |
826 |
COEND |
|
53241 | 827 |
\<lbrace>False\<rbrace>" |
13020 | 828 |
apply oghoare |
829 |
apply(force simp add: Mutator_def Collector_def modules) |
|
830 |
apply(rule Collector) |
|
831 |
apply(rule Mutator) |
|
832 |
apply(simp add:interfree_Collector_Mutator) |
|
833 |
apply(simp add:interfree_Mutator_Collector) |
|
834 |
apply force |
|
835 |
done |
|
836 |
||
837 |
end |