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