58 thus "valid_trace (e # s)" by (unfold_locales, simp) |
65 thus "valid_trace (e # s)" by (unfold_locales, simp) |
59 qed (insert h, auto) |
66 qed (insert h, auto) |
60 qed |
67 qed |
61 |
68 |
62 lemma wq_distinct: "distinct (wq s cs)" |
69 lemma wq_distinct: "distinct (wq s cs)" |
63 proof(rule ind, simp add:wq_def) |
70 proof(induct rule:ind) |
64 fix s e |
71 case (Cons s e) |
65 assume h1: "step s e" |
72 from Cons(4,3) |
66 and h2: "distinct (wq s cs)" |
73 show ?case |
67 thus "distinct (wq (e # s) cs)" |
74 proof(induct) |
68 proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits) |
75 case (thread_P th s cs1) |
69 fix thread s |
76 show ?case |
70 assume h1: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+" |
77 proof(cases "cs = cs1") |
71 and h2: "thread \<in> set (wq_fun (schs s) cs)" |
78 case True |
72 and h3: "thread \<in> runing s" |
79 thus ?thesis (is "distinct ?L") |
73 show "False" |
80 proof - |
74 proof - |
81 have "?L = wq_fun (schs s) cs1 @ [th]" using True |
75 from h3 have "\<And> cs. thread \<in> set (wq_fun (schs s) cs) \<Longrightarrow> |
82 by (simp add:wq_def wf_def Let_def split:list.splits) |
76 thread = hd ((wq_fun (schs s) cs))" |
83 moreover have "distinct ..." |
77 by (simp add:runing_def readys_def s_waiting_def wq_def) |
84 proof - |
78 from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" . |
85 have "th \<notin> set (wq_fun (schs s) cs1)" |
79 with h2 |
86 proof |
80 have "(Cs cs, Th thread) \<in> (RAG s)" |
87 assume otherwise: "th \<in> set (wq_fun (schs s) cs1)" |
81 by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def) |
88 from runing_head[OF thread_P(1) this] |
82 with h1 show False by auto |
89 have "th = hd (wq_fun (schs s) cs1)" . |
|
90 hence "(Cs cs1, Th th) \<in> (RAG s)" using otherwise |
|
91 by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def) |
|
92 with thread_P(2) show False by auto |
|
93 qed |
|
94 moreover have "distinct (wq_fun (schs s) cs1)" |
|
95 using True thread_P wq_def by auto |
|
96 ultimately show ?thesis by auto |
|
97 qed |
|
98 ultimately show ?thesis by simp |
|
99 qed |
|
100 next |
|
101 case False |
|
102 with thread_P(3) |
|
103 show ?thesis |
|
104 by (auto simp:wq_def wf_def Let_def split:list.splits) |
83 qed |
105 qed |
84 next |
106 next |
85 fix thread s a list |
107 case (thread_V th s cs1) |
86 assume dst: "distinct list" |
108 thus ?case |
87 show "distinct (SOME q. distinct q \<and> set q = set list)" |
109 proof(cases "cs = cs1") |
88 proof(rule someI2) |
110 case True |
89 from dst show "distinct list \<and> set list = set list" by auto |
111 show ?thesis (is "distinct ?L") |
90 next |
112 proof(cases "(wq s cs)") |
91 fix q assume "distinct q \<and> set q = set list" |
113 case Nil |
92 thus "distinct q" by auto |
114 thus ?thesis |
93 qed |
115 by (auto simp:wq_def wf_def Let_def split:list.splits) |
94 qed |
116 next |
95 qed |
117 case (Cons w_hd w_tl) |
|
118 moreover have "distinct (SOME q. distinct q \<and> set q = set w_tl)" |
|
119 proof(rule someI2) |
|
120 from thread_V(3)[unfolded Cons] |
|
121 show "distinct w_tl \<and> set w_tl = set w_tl" by auto |
|
122 qed auto |
|
123 ultimately show ?thesis |
|
124 by (auto simp:wq_def wf_def Let_def True split:list.splits) |
|
125 qed |
|
126 next |
|
127 case False |
|
128 with thread_V(3) |
|
129 show ?thesis |
|
130 by (auto simp:wq_def wf_def Let_def split:list.splits) |
|
131 qed |
|
132 qed (insert Cons, auto simp: wq_def Let_def split:list.splits) |
|
133 qed (unfold wq_def Let_def, simp) |
96 |
134 |
97 end |
135 end |
98 |
136 |
99 |
137 |
100 context valid_trace_e |
138 context valid_trace_e |
106 Such kind of lemmas are very obvious, but need to be checked formally. |
144 Such kind of lemmas are very obvious, but need to be checked formally. |
107 This is a kind of confirmation that our modelling is correct. |
145 This is a kind of confirmation that our modelling is correct. |
108 *} |
146 *} |
109 |
147 |
110 lemma block_pre: |
148 lemma block_pre: |
111 assumes s_ni: "thread \<notin> set (wq s cs)" |
149 assumes s_ni: "thread \<notin> set (wq s cs)" |
112 and s_i: "thread \<in> set (wq (e#s) cs)" |
150 and s_i: "thread \<in> set (wq (e#s) cs)" |
113 shows "e = P thread cs" |
151 shows "e = P thread cs" |
114 proof - |
152 proof(cases e) |
115 show ?thesis |
153 -- {* This is the only non-trivial case: *} |
116 proof(cases e) |
154 case (V th cs1) |
117 case (P th cs) |
155 have False |
118 with assms |
156 proof(cases "cs1 = cs") |
|
157 case True |
119 show ?thesis |
158 show ?thesis |
120 by (auto simp:wq_def Let_def split:if_splits) |
159 proof(cases "(wq s cs1)") |
121 next |
160 case (Cons w_hd w_tl) |
122 case (Create th prio) |
161 have "set (wq (e#s) cs) \<subseteq> set (wq s cs)" |
123 with assms show ?thesis |
|
124 by (auto simp:wq_def Let_def split:if_splits) |
|
125 next |
|
126 case (Exit th) |
|
127 with assms show ?thesis |
|
128 by (auto simp:wq_def Let_def split:if_splits) |
|
129 next |
|
130 case (Set th prio) |
|
131 with assms show ?thesis |
|
132 by (auto simp:wq_def Let_def split:if_splits) |
|
133 next |
|
134 case (V th cs) |
|
135 with vt_e assms show ?thesis |
|
136 apply (auto simp:wq_def Let_def split:if_splits) |
|
137 proof - |
|
138 fix q qs |
|
139 assume h1: "thread \<notin> set (wq_fun (schs s) cs)" |
|
140 and h2: "q # qs = wq_fun (schs s) cs" |
|
141 and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)" |
|
142 and vt: "vt (V th cs # s)" |
|
143 from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp |
|
144 moreover have "thread \<in> set qs" |
|
145 proof - |
162 proof - |
146 have "set (SOME q. distinct q \<and> set q = set qs) = set qs" |
163 have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)" |
|
164 using Cons V by (auto simp:wq_def Let_def True split:if_splits) |
|
165 moreover have "set ... \<subseteq> set (wq s cs)" |
147 proof(rule someI2) |
166 proof(rule someI2) |
148 from wq_distinct [of cs] |
167 show "distinct w_tl \<and> set w_tl = set w_tl" |
149 and h2[symmetric, folded wq_def] |
168 by (metis distinct.simps(2) local.Cons wq_distinct) |
150 show "distinct qs \<and> set qs = set qs" by auto |
169 qed (insert Cons True, auto) |
151 next |
170 ultimately show ?thesis by simp |
152 fix x assume "distinct x \<and> set x = set qs" |
171 qed |
153 thus "set x = set qs" by auto |
172 with assms show ?thesis by auto |
154 qed |
173 qed (insert assms V True, auto simp:wq_def Let_def split:if_splits) |
155 with h3 show ?thesis by simp |
174 qed (insert assms V, auto simp:wq_def Let_def split:if_splits) |
156 qed |
175 thus ?thesis by auto |
157 ultimately show "False" by auto |
176 qed (insert assms, auto simp:wq_def Let_def split:if_splits) |
158 qed |
|
159 qed |
|
160 qed |
|
161 |
177 |
162 end |
178 end |
163 |
179 |
164 text {* |
180 text {* |
165 The following lemmas is also obvious and shallow. It says |
181 The following lemmas is also obvious and shallow. It says |
258 show ?thesis by simp |
274 show ?thesis by simp |
259 qed |
275 qed |
260 ultimately show ?thesis by simp |
276 ultimately show ?thesis by simp |
261 qed |
277 qed |
262 qed |
278 qed |
263 |
279 end |
264 (* Wrong: |
280 |
265 lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2" |
281 locale valid_moment = valid_trace + |
266 *) |
282 fixes i :: nat |
|
283 |
|
284 sublocale valid_moment < vat_moment: valid_trace "(moment i s)" |
|
285 by (unfold_locales, insert vt_moment, auto) |
|
286 |
|
287 context valid_trace |
|
288 begin |
|
289 |
267 |
290 |
268 text {* (* ddd *) |
291 text {* (* ddd *) |
269 The nature of the work is like this: since it starts from a very simple and basic |
292 The nature of the work is like this: since it starts from a very simple and basic |
270 model, even intuitively very `basic` and `obvious` properties need to derived from scratch. |
293 model, even intuitively very `basic` and `obvious` properties need to derived from scratch. |
271 For instance, the fact |
294 For instance, the fact |
290 @{text "p_split"} to these two blocking facts, there exist |
313 @{text "p_split"} to these two blocking facts, there exist |
291 two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that |
314 two moments @{text "t1"} and @{text "t2"} in @{text "s"}, such that |
292 @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} |
315 @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} |
293 and kept on blocked on them respectively ever since. |
316 and kept on blocked on them respectively ever since. |
294 |
317 |
295 Without lose of generality, we assume @{text "t1"} is earlier than @{text "t2"}. |
318 Without lost of generality, we assume @{text "t1"} is earlier than @{text "t2"}. |
296 However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still |
319 However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still |
297 in blocked state at moment @{text "t2"} and could not |
320 in blocked state at moment @{text "t2"} and could not |
298 make any request and get blocked the second time: Contradiction. |
321 make any request and get blocked the second time: Contradiction. |
299 *} |
322 *} |
300 |
323 |
301 lemma waiting_unique_pre: |
324 lemma waiting_unique_pre: (* ccc *) |
302 assumes h11: "thread \<in> set (wq s cs1)" |
325 assumes h11: "thread \<in> set (wq s cs1)" |
303 and h12: "thread \<noteq> hd (wq s cs1)" |
326 and h12: "thread \<noteq> hd (wq s cs1)" |
304 assumes h21: "thread \<in> set (wq s cs2)" |
327 assumes h21: "thread \<in> set (wq s cs2)" |
305 and h22: "thread \<noteq> hd (wq s cs2)" |
328 and h22: "thread \<noteq> hd (wq s cs2)" |
306 and neq12: "cs1 \<noteq> cs2" |
329 and neq12: "cs1 \<noteq> cs2" |
517 thus ?thesis by auto |
540 thus ?thesis by auto |
518 qed |
541 qed |
519 |
542 |
520 (* An aux lemma used later *) |
543 (* An aux lemma used later *) |
521 lemma unique_minus: |
544 lemma unique_minus: |
522 fixes x y z r |
|
523 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
545 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
524 and xy: "(x, y) \<in> r" |
546 and xy: "(x, y) \<in> r" |
525 and xz: "(x, z) \<in> r^+" |
547 and xz: "(x, z) \<in> r^+" |
526 and neq: "y \<noteq> z" |
548 and neq: "y \<noteq> z" |
527 shows "(y, z) \<in> r^+" |
549 shows "(y, z) \<in> r^+" |
545 qed |
567 qed |
546 qed |
568 qed |
547 qed |
569 qed |
548 |
570 |
549 lemma unique_base: |
571 lemma unique_base: |
550 fixes r x y z |
|
551 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
572 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
552 and xy: "(x, y) \<in> r" |
573 and xy: "(x, y) \<in> r" |
553 and xz: "(x, z) \<in> r^+" |
574 and xz: "(x, z) \<in> r^+" |
554 and neq_yz: "y \<noteq> z" |
575 and neq_yz: "y \<noteq> z" |
555 shows "(y, z) \<in> r^+" |
576 shows "(y, z) \<in> r^+" |
572 qed |
593 qed |
573 qed |
594 qed |
574 qed |
595 qed |
575 |
596 |
576 lemma unique_chain: |
597 lemma unique_chain: |
577 fixes r x y z |
|
578 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
598 assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c" |
579 and xy: "(x, y) \<in> r^+" |
599 and xy: "(x, y) \<in> r^+" |
580 and xz: "(x, z) \<in> r^+" |
600 and xz: "(x, z) \<in> r^+" |
581 and neq_yz: "y \<noteq> z" |
601 and neq_yz: "y \<noteq> z" |
582 shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+" |
602 shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+" |
1340 lemma range_in: "\<lbrakk>(Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s" |
1359 lemma range_in: "\<lbrakk>(Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s" |
1341 apply(unfold s_RAG_def cs_waiting_def cs_holding_def) |
1360 apply(unfold s_RAG_def cs_waiting_def cs_holding_def) |
1342 by (auto intro:wq_threads) |
1361 by (auto intro:wq_threads) |
1343 |
1362 |
1344 lemma readys_v_eq: |
1363 lemma readys_v_eq: |
1345 fixes th thread cs rest |
|
1346 assumes neq_th: "th \<noteq> thread" |
1364 assumes neq_th: "th \<noteq> thread" |
1347 and eq_wq: "wq s cs = thread#rest" |
1365 and eq_wq: "wq s cs = thread#rest" |
1348 and not_in: "th \<notin> set rest" |
1366 and not_in: "th \<notin> set rest" |
1349 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)" |
1367 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)" |
1350 proof - |
1368 proof - |
1509 |
1527 |
1510 end |
1528 end |
1511 |
1529 |
1512 |
1530 |
1513 lemma step_holdents_p_add: |
1531 lemma step_holdents_p_add: |
1514 fixes th cs s |
|
1515 assumes vt: "vt (P th cs#s)" |
1532 assumes vt: "vt (P th cs#s)" |
1516 and "wq s cs = []" |
1533 and "wq s cs = []" |
1517 shows "holdents (P th cs#s) th = holdents s th \<union> {cs}" |
1534 shows "holdents (P th cs#s) th = holdents s th \<union> {cs}" |
1518 proof - |
1535 proof - |
1519 from assms show ?thesis |
1536 from assms show ?thesis |
1520 unfolding holdents_test step_RAG_p[OF vt] by (auto) |
1537 unfolding holdents_test step_RAG_p[OF vt] by (auto) |
1521 qed |
1538 qed |
1522 |
1539 |
1523 lemma step_holdents_p_eq: |
1540 lemma step_holdents_p_eq: |
1524 fixes th cs s |
|
1525 assumes vt: "vt (P th cs#s)" |
1541 assumes vt: "vt (P th cs#s)" |
1526 and "wq s cs \<noteq> []" |
1542 and "wq s cs \<noteq> []" |
1527 shows "holdents (P th cs#s) th = holdents s th" |
1543 shows "holdents (P th cs#s) th = holdents s th" |
1528 proof - |
1544 proof - |
1529 from assms show ?thesis |
1545 from assms show ?thesis |