262
+ − 1
theory CpsG
+ − 2
imports PrioG
+ − 3
begin
+ − 4
+ − 5
lemma not_thread_holdents:
+ − 6
fixes th s
+ − 7
assumes vt: "vt step s"
+ − 8
and not_in: "th \<notin> threads s"
+ − 9
shows "holdents s th = {}"
+ − 10
proof -
+ − 11
from vt not_in show ?thesis
+ − 12
proof(induct arbitrary:th)
+ − 13
case (vt_cons s e th)
+ − 14
assume vt: "vt step s"
+ − 15
and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"
+ − 16
and stp: "step s e"
+ − 17
and not_in: "th \<notin> threads (e # s)"
+ − 18
from stp show ?case
+ − 19
proof(cases)
+ − 20
case (thread_create thread prio)
+ − 21
assume eq_e: "e = Create thread prio"
+ − 22
and not_in': "thread \<notin> threads s"
+ − 23
have "holdents (e # s) th = holdents s th"
+ − 24
apply (unfold eq_e holdents_def)
+ − 25
by (simp add:depend_create_unchanged)
+ − 26
moreover have "th \<notin> threads s"
+ − 27
proof -
+ − 28
from not_in eq_e show ?thesis by simp
+ − 29
qed
+ − 30
moreover note ih ultimately show ?thesis by auto
+ − 31
next
+ − 32
case (thread_exit thread)
+ − 33
assume eq_e: "e = Exit thread"
+ − 34
and nh: "holdents s thread = {}"
+ − 35
show ?thesis
+ − 36
proof(cases "th = thread")
+ − 37
case True
+ − 38
with nh eq_e
+ − 39
show ?thesis
+ − 40
by (auto simp:holdents_def depend_exit_unchanged)
+ − 41
next
+ − 42
case False
+ − 43
with not_in and eq_e
+ − 44
have "th \<notin> threads s" by simp
+ − 45
from ih[OF this] False eq_e show ?thesis
+ − 46
by (auto simp:holdents_def depend_exit_unchanged)
+ − 47
qed
+ − 48
next
+ − 49
case (thread_P thread cs)
+ − 50
assume eq_e: "e = P thread cs"
+ − 51
and is_runing: "thread \<in> runing s"
+ − 52
from prems have vtp: "vt step (P thread cs#s)" by auto
+ − 53
have neq_th: "th \<noteq> thread"
+ − 54
proof -
+ − 55
from not_in eq_e have "th \<notin> threads s" by simp
+ − 56
moreover from is_runing have "thread \<in> threads s"
+ − 57
by (simp add:runing_def readys_def)
+ − 58
ultimately show ?thesis by auto
+ − 59
qed
+ − 60
hence "holdents (e # s) th = holdents s th "
+ − 61
apply (unfold cntCS_def holdents_def eq_e)
+ − 62
by (unfold step_depend_p[OF vtp], auto)
+ − 63
moreover have "holdents s th = {}"
+ − 64
proof(rule ih)
+ − 65
from not_in eq_e show "th \<notin> threads s" by simp
+ − 66
qed
+ − 67
ultimately show ?thesis by simp
+ − 68
next
+ − 69
case (thread_V thread cs)
+ − 70
assume eq_e: "e = V thread cs"
+ − 71
and is_runing: "thread \<in> runing s"
+ − 72
and hold: "holding s thread cs"
+ − 73
have neq_th: "th \<noteq> thread"
+ − 74
proof -
+ − 75
from not_in eq_e have "th \<notin> threads s" by simp
+ − 76
moreover from is_runing have "thread \<in> threads s"
+ − 77
by (simp add:runing_def readys_def)
+ − 78
ultimately show ?thesis by auto
+ − 79
qed
+ − 80
from prems have vtv: "vt step (V thread cs#s)" by auto
+ − 81
from hold obtain rest
+ − 82
where eq_wq: "wq s cs = thread # rest"
+ − 83
by (case_tac "wq s cs", auto simp:s_holding_def)
+ − 84
from not_in eq_e eq_wq
+ − 85
have "\<not> next_th s thread cs th"
+ − 86
apply (auto simp:next_th_def)
+ − 87
proof -
+ − 88
assume ne: "rest \<noteq> []"
+ − 89
and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
+ − 90
have "?t \<in> set rest"
+ − 91
proof(rule someI2)
+ − 92
from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
+ − 93
show "distinct rest \<and> set rest = set rest" by auto
+ − 94
next
+ − 95
fix x assume "distinct x \<and> set x = set rest" with ne
+ − 96
show "hd x \<in> set rest" by (cases x, auto)
+ − 97
qed
+ − 98
with eq_wq have "?t \<in> set (wq s cs)" by simp
+ − 99
from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
+ − 100
show False by auto
+ − 101
qed
+ − 102
moreover note neq_th eq_wq
+ − 103
ultimately have "holdents (e # s) th = holdents s th"
+ − 104
by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto)
+ − 105
moreover have "holdents s th = {}"
+ − 106
proof(rule ih)
+ − 107
from not_in eq_e show "th \<notin> threads s" by simp
+ − 108
qed
+ − 109
ultimately show ?thesis by simp
+ − 110
next
+ − 111
case (thread_set thread prio)
+ − 112
print_facts
+ − 113
assume eq_e: "e = Set thread prio"
+ − 114
and is_runing: "thread \<in> runing s"
+ − 115
from not_in and eq_e have "th \<notin> threads s" by auto
+ − 116
from ih [OF this] and eq_e
+ − 117
show ?thesis
+ − 118
apply (unfold eq_e cntCS_def holdents_def)
+ − 119
by (simp add:depend_set_unchanged)
+ − 120
qed
+ − 121
next
+ − 122
case vt_nil
+ − 123
show ?case
+ − 124
by (auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
+ − 125
qed
+ − 126
qed
+ − 127
+ − 128
+ − 129
+ − 130
lemma next_th_neq:
+ − 131
assumes vt: "vt step s"
+ − 132
and nt: "next_th s th cs th'"
+ − 133
shows "th' \<noteq> th"
+ − 134
proof -
+ − 135
from nt show ?thesis
+ − 136
apply (auto simp:next_th_def)
+ − 137
proof -
+ − 138
fix rest
+ − 139
assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
+ − 140
and ne: "rest \<noteq> []"
+ − 141
have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest"
+ − 142
proof(rule someI2)
+ − 143
from wq_distinct[OF vt, of cs] eq_wq
+ − 144
show "distinct rest \<and> set rest = set rest" by auto
+ − 145
next
+ − 146
fix x
+ − 147
assume "distinct x \<and> set x = set rest"
+ − 148
hence eq_set: "set x = set rest" by auto
+ − 149
with ne have "x \<noteq> []" by auto
+ − 150
hence "hd x \<in> set x" by auto
+ − 151
with eq_set show "hd x \<in> set rest" by auto
+ − 152
qed
+ − 153
with wq_distinct[OF vt, of cs] eq_wq show False by auto
+ − 154
qed
+ − 155
qed
+ − 156
+ − 157
lemma next_th_unique:
+ − 158
assumes nt1: "next_th s th cs th1"
+ − 159
and nt2: "next_th s th cs th2"
+ − 160
shows "th1 = th2"
+ − 161
proof -
+ − 162
from assms show ?thesis
+ − 163
by (unfold next_th_def, auto)
+ − 164
qed
+ − 165
+ − 166
lemma pp_sub: "(r^+)^+ \<subseteq> r^+"
+ − 167
by auto
+ − 168
+ − 169
lemma wf_depend:
+ − 170
assumes vt: "vt step s"
+ − 171
shows "wf (depend s)"
+ − 172
proof(rule finite_acyclic_wf)
+ − 173
from finite_depend[OF vt] show "finite (depend s)" .
+ − 174
next
+ − 175
from acyclic_depend[OF vt] show "acyclic (depend s)" .
+ − 176
qed
+ − 177
+ − 178
lemma Max_Union:
+ − 179
assumes fc: "finite C"
+ − 180
and ne: "C \<noteq> {}"
+ − 181
and fa: "\<And> A. A \<in> C \<Longrightarrow> finite A \<and> A \<noteq> {}"
+ − 182
shows "Max (\<Union> C) = Max (Max ` C)"
+ − 183
proof -
+ − 184
from fc ne fa show ?thesis
+ − 185
proof(induct)
+ − 186
case (insert x F)
+ − 187
assume ih: "\<lbrakk>F \<noteq> {}; \<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}\<rbrakk> \<Longrightarrow> Max (\<Union>F) = Max (Max ` F)"
+ − 188
and h: "\<And> A. A \<in> insert x F \<Longrightarrow> finite A \<and> A \<noteq> {}"
+ − 189
show ?case (is "?L = ?R")
+ − 190
proof(cases "F = {}")
+ − 191
case False
+ − 192
from Union_insert have "?L = Max (x \<union> (\<Union> F))" by simp
+ − 193
also have "\<dots> = max (Max x) (Max(\<Union> F))"
+ − 194
proof(rule Max_Un)
+ − 195
from h[of x] show "finite x" by auto
+ − 196
next
+ − 197
from h[of x] show "x \<noteq> {}" by auto
+ − 198
next
+ − 199
show "finite (\<Union>F)"
+ − 200
proof(rule finite_Union)
+ − 201
show "finite F" by fact
+ − 202
next
+ − 203
from h show "\<And>M. M \<in> F \<Longrightarrow> finite M" by auto
+ − 204
qed
+ − 205
next
+ − 206
from False and h show "\<Union>F \<noteq> {}" by auto
+ − 207
qed
+ − 208
also have "\<dots> = ?R"
+ − 209
proof -
+ − 210
have "?R = Max (Max ` ({x} \<union> F))" by simp
+ − 211
also have "\<dots> = Max ({Max x} \<union> (Max ` F))" by simp
+ − 212
also have "\<dots> = max (Max x) (Max (\<Union>F))"
+ − 213
proof -
+ − 214
have "Max ({Max x} \<union> Max ` F) = max (Max {Max x}) (Max (Max ` F))"
+ − 215
proof(rule Max_Un)
+ − 216
show "finite {Max x}" by simp
+ − 217
next
+ − 218
show "{Max x} \<noteq> {}" by simp
+ − 219
next
+ − 220
from insert show "finite (Max ` F)" by auto
+ − 221
next
+ − 222
from False show "Max ` F \<noteq> {}" by auto
+ − 223
qed
+ − 224
moreover have "Max {Max x} = Max x" by simp
+ − 225
moreover have "Max (\<Union>F) = Max (Max ` F)"
+ − 226
proof(rule ih)
+ − 227
show "F \<noteq> {}" by fact
+ − 228
next
+ − 229
from h show "\<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}"
+ − 230
by auto
+ − 231
qed
+ − 232
ultimately show ?thesis by auto
+ − 233
qed
+ − 234
finally show ?thesis by simp
+ − 235
qed
+ − 236
finally show ?thesis by simp
+ − 237
next
+ − 238
case True
+ − 239
thus ?thesis by auto
+ − 240
qed
+ − 241
next
+ − 242
case empty
+ − 243
assume "{} \<noteq> {}" show ?case by auto
+ − 244
qed
+ − 245
qed
+ − 246
+ − 247
definition child :: "state \<Rightarrow> (node \<times> node) set"
+ − 248
where "child s =
+ − 249
{(Th th', Th th) | th th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend s}"
+ − 250
+ − 251
definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
+ − 252
where "children s th = {th'. (Th th', Th th) \<in> child s}"
+ − 253
+ − 254
+ − 255
lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"
+ − 256
by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
+ − 257
+ − 258
lemma child_unique:
+ − 259
assumes vt: "vt step s"
+ − 260
and ch1: "(Th th, Th th1) \<in> child s"
+ − 261
and ch2: "(Th th, Th th2) \<in> child s"
+ − 262
shows "th1 = th2"
+ − 263
proof -
+ − 264
from ch1 ch2 show ?thesis
+ − 265
proof(unfold child_def, clarsimp)
+ − 266
fix cs csa
+ − 267
assume h1: "(Th th, Cs cs) \<in> depend s"
+ − 268
and h2: "(Cs cs, Th th1) \<in> depend s"
+ − 269
and h3: "(Th th, Cs csa) \<in> depend s"
+ − 270
and h4: "(Cs csa, Th th2) \<in> depend s"
+ − 271
from unique_depend[OF vt h1 h3] have "cs = csa" by simp
+ − 272
with h4 have "(Cs cs, Th th2) \<in> depend s" by simp
+ − 273
from unique_depend[OF vt h2 this]
+ − 274
show "th1 = th2" by simp
+ − 275
qed
+ − 276
qed
+ − 277
+ − 278
+ − 279
lemma cp_eq_cpreced_f: "cp s = cpreced s (wq s)"
+ − 280
proof -
+ − 281
from fun_eq_iff
+ − 282
have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto
+ − 283
show ?thesis
+ − 284
proof(rule h)
+ − 285
from cp_eq_cpreced show "\<forall>x. cp s x = cpreced s (wq s) x" by auto
+ − 286
qed
+ − 287
qed
+ − 288
+ − 289
lemma depend_children:
+ − 290
assumes h: "(Th th1, Th th2) \<in> (depend s)^+"
+ − 291
shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)^+)"
+ − 292
proof -
+ − 293
from h show ?thesis
+ − 294
proof(induct rule: tranclE)
+ − 295
fix c th2
+ − 296
assume h1: "(Th th1, c) \<in> (depend s)\<^sup>+"
+ − 297
and h2: "(c, Th th2) \<in> depend s"
+ − 298
from h2 obtain cs where eq_c: "c = Cs cs"
+ − 299
by (case_tac c, auto simp:s_depend_def)
+ − 300
show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"
+ − 301
proof(rule tranclE[OF h1])
+ − 302
fix ca
+ − 303
assume h3: "(Th th1, ca) \<in> (depend s)\<^sup>+"
+ − 304
and h4: "(ca, c) \<in> depend s"
+ − 305
show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"
+ − 306
proof -
+ − 307
from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
+ − 308
by (case_tac ca, auto simp:s_depend_def)
+ − 309
from eq_ca h4 h2 eq_c
+ − 310
have "th3 \<in> children s th2" by (auto simp:children_def child_def)
+ − 311
moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (depend s)\<^sup>+" by simp
+ − 312
ultimately show ?thesis by auto
+ − 313
qed
+ − 314
next
+ − 315
assume "(Th th1, c) \<in> depend s"
+ − 316
with h2 eq_c
+ − 317
have "th1 \<in> children s th2"
+ − 318
by (auto simp:children_def child_def)
+ − 319
thus ?thesis by auto
+ − 320
qed
+ − 321
next
+ − 322
assume "(Th th1, Th th2) \<in> depend s"
+ − 323
thus ?thesis
+ − 324
by (auto simp:s_depend_def)
+ − 325
qed
+ − 326
qed
+ − 327
+ − 328
lemma sub_child: "child s \<subseteq> (depend s)^+"
+ − 329
by (unfold child_def, auto)
+ − 330
+ − 331
lemma wf_child:
+ − 332
assumes vt: "vt step s"
+ − 333
shows "wf (child s)"
+ − 334
proof(rule wf_subset)
+ − 335
from wf_trancl[OF wf_depend[OF vt]]
+ − 336
show "wf ((depend s)\<^sup>+)" .
+ − 337
next
+ − 338
from sub_child show "child s \<subseteq> (depend s)\<^sup>+" .
+ − 339
qed
+ − 340
+ − 341
lemma depend_child_pre:
+ − 342
assumes vt: "vt step s"
+ − 343
shows
+ − 344
"(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
+ − 345
proof -
+ − 346
from wf_trancl[OF wf_depend[OF vt]]
+ − 347
have wf: "wf ((depend s)^+)" .
+ − 348
show ?thesis
+ − 349
proof(rule wf_induct[OF wf, of ?P], clarsimp)
+ − 350
fix th'
+ − 351
assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (depend s)\<^sup>+ \<longrightarrow>
+ − 352
(Th th, y) \<in> (depend s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
+ − 353
and h: "(Th th, Th th') \<in> (depend s)\<^sup>+"
+ − 354
show "(Th th, Th th') \<in> (child s)\<^sup>+"
+ − 355
proof -
+ − 356
from depend_children[OF h]
+ − 357
have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend s)\<^sup>+)" .
+ − 358
thus ?thesis
+ − 359
proof
+ − 360
assume "th \<in> children s th'"
+ − 361
thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
+ − 362
next
+ − 363
assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend s)\<^sup>+"
+ − 364
then obtain th3 where th3_in: "th3 \<in> children s th'"
+ − 365
and th_dp: "(Th th, Th th3) \<in> (depend s)\<^sup>+" by auto
+ − 366
from th3_in have "(Th th3, Th th') \<in> (depend s)^+" by (auto simp:children_def child_def)
+ − 367
from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp
+ − 368
with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
+ − 369
qed
+ − 370
qed
+ − 371
qed
+ − 372
qed
+ − 373
+ − 374
lemma depend_child: "\<lbrakk>vt step s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
+ − 375
by (insert depend_child_pre, auto)
+ − 376
+ − 377
lemma child_depend_p:
+ − 378
assumes "(n1, n2) \<in> (child s)^+"
+ − 379
shows "(n1, n2) \<in> (depend s)^+"
+ − 380
proof -
+ − 381
from assms show ?thesis
+ − 382
proof(induct)
+ − 383
case (base y)
+ − 384
with sub_child show ?case by auto
+ − 385
next
+ − 386
case (step y z)
+ − 387
assume "(y, z) \<in> child s"
+ − 388
with sub_child have "(y, z) \<in> (depend s)^+" by auto
+ − 389
moreover have "(n1, y) \<in> (depend s)^+" by fact
+ − 390
ultimately show ?case by auto
+ − 391
qed
+ − 392
qed
+ − 393
+ − 394
lemma child_depend_eq:
+ − 395
assumes vt: "vt step s"
+ − 396
shows
+ − 397
"((Th th1, Th th2) \<in> (child s)^+) =
+ − 398
((Th th1, Th th2) \<in> (depend s)^+)"
+ − 399
by (auto intro: depend_child[OF vt] child_depend_p)
+ − 400
+ − 401
lemma children_no_dep:
+ − 402
fixes s th th1 th2 th3
+ − 403
assumes vt: "vt step s"
+ − 404
and ch1: "(Th th1, Th th) \<in> child s"
+ − 405
and ch2: "(Th th2, Th th) \<in> child s"
+ − 406
and ch3: "(Th th1, Th th2) \<in> (depend s)^+"
+ − 407
shows "False"
+ − 408
proof -
+ − 409
from depend_child[OF vt ch3]
+ − 410
have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
+ − 411
thus ?thesis
+ − 412
proof(rule converse_tranclE)
+ − 413
thm tranclD
+ − 414
assume "(Th th1, Th th2) \<in> child s"
+ − 415
from child_unique[OF vt ch1 this] have "th = th2" by simp
+ − 416
with ch2 have "(Th th2, Th th2) \<in> child s" by simp
+ − 417
with wf_child[OF vt] show ?thesis by auto
+ − 418
next
+ − 419
fix c
+ − 420
assume h1: "(Th th1, c) \<in> child s"
+ − 421
and h2: "(c, Th th2) \<in> (child s)\<^sup>+"
+ − 422
from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)
+ − 423
with h1 have "(Th th1, Th th3) \<in> child s" by simp
+ − 424
from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp
+ − 425
with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp
+ − 426
with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto
+ − 427
moreover have "wf ((child s)\<^sup>+)"
+ − 428
proof(rule wf_trancl)
+ − 429
from wf_child[OF vt] show "wf (child s)" .
+ − 430
qed
+ − 431
ultimately show False by auto
+ − 432
qed
+ − 433
qed
+ − 434
+ − 435
lemma unique_depend_p:
+ − 436
assumes vt: "vt step s"
+ − 437
and dp1: "(n, n1) \<in> (depend s)^+"
+ − 438
and dp2: "(n, n2) \<in> (depend s)^+"
+ − 439
and neq: "n1 \<noteq> n2"
+ − 440
shows "(n1, n2) \<in> (depend s)^+ \<or> (n2, n1) \<in> (depend s)^+"
+ − 441
proof(rule unique_chain [OF _ dp1 dp2 neq])
+ − 442
from unique_depend[OF vt]
+ − 443
show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by auto
+ − 444
qed
+ − 445
+ − 446
lemma dependents_child_unique:
+ − 447
fixes s th th1 th2 th3
+ − 448
assumes vt: "vt step s"
+ − 449
and ch1: "(Th th1, Th th) \<in> child s"
+ − 450
and ch2: "(Th th2, Th th) \<in> child s"
+ − 451
and dp1: "th3 \<in> dependents s th1"
+ − 452
and dp2: "th3 \<in> dependents s th2"
+ − 453
shows "th1 = th2"
+ − 454
proof -
+ − 455
{ assume neq: "th1 \<noteq> th2"
+ − 456
from dp1 have dp1: "(Th th3, Th th1) \<in> (depend s)^+"
+ − 457
by (simp add:s_dependents_def eq_depend)
+ − 458
from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+"
+ − 459
by (simp add:s_dependents_def eq_depend)
+ − 460
from unique_depend_p[OF vt dp1 dp2] and neq
+ − 461
have "(Th th1, Th th2) \<in> (depend s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (depend s)\<^sup>+" by auto
+ − 462
hence False
+ − 463
proof
+ − 464
assume "(Th th1, Th th2) \<in> (depend s)\<^sup>+ "
+ − 465
from children_no_dep[OF vt ch1 ch2 this] show ?thesis .
+ − 466
next
+ − 467
assume " (Th th2, Th th1) \<in> (depend s)\<^sup>+"
+ − 468
from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
+ − 469
qed
+ − 470
} thus ?thesis by auto
+ − 471
qed
+ − 472
+ − 473
lemma cp_rec:
+ − 474
fixes s th
+ − 475
assumes vt: "vt step s"
+ − 476
shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
+ − 477
proof(unfold cp_eq_cpreced_f cpreced_def)
+ − 478
let ?f = "(\<lambda>th. preced th s)"
+ − 479
show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
+ − 480
Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th)"
+ − 481
proof(cases " children s th = {}")
+ − 482
case False
+ − 483
have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th =
+ − 484
{Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
+ − 485
(is "?L = ?R")
+ − 486
by auto
+ − 487
also have "\<dots> =
+ − 488
Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"
+ − 489
(is "_ = Max ` ?C")
+ − 490
by auto
+ − 491
finally have "Max ?L = Max (Max ` ?C)" by auto
+ − 492
also have "\<dots> = Max (\<Union> ?C)"
+ − 493
proof(rule Max_Union[symmetric])
+ − 494
from children_dependents[of s th] finite_threads[OF vt] and dependents_threads[OF vt, of th]
+ − 495
show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ − 496
by (auto simp:finite_subset)
+ − 497
next
+ − 498
from False
+ − 499
show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"
+ − 500
by simp
+ − 501
next
+ − 502
show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>
+ − 503
finite A \<and> A \<noteq> {}"
+ − 504
apply (auto simp:finite_subset)
+ − 505
proof -
+ − 506
fix th'
+ − 507
from finite_threads[OF vt] and dependents_threads[OF vt, of th']
+ − 508
show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th')" by (auto simp:finite_subset)
+ − 509
qed
+ − 510
qed
+ − 511
also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependents (wq s) th)"
+ − 512
(is "Max ?A = Max ?B")
+ − 513
proof -
+ − 514
have "?A = ?B"
+ − 515
proof
+ − 516
show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}
+ − 517
\<subseteq> (\<lambda>th. preced th s) ` dependents (wq s) th"
+ − 518
proof
+ − 519
fix x
+ − 520
assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ − 521
then obtain th' where
+ − 522
th'_in: "th' \<in> children s th"
+ − 523
and x_in: "x \<in> ?f ` ({th'} \<union> dependents (wq s) th')" by auto
+ − 524
hence "x = ?f th' \<or> x \<in> (?f ` dependents (wq s) th')" by auto
+ − 525
thus "x \<in> ?f ` dependents (wq s) th"
+ − 526
proof
+ − 527
assume "x = preced th' s"
+ − 528
with th'_in and children_dependents
+ − 529
show "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th" by auto
+ − 530
next
+ − 531
assume "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th'"
+ − 532
moreover note th'_in
+ − 533
ultimately show " x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
+ − 534
by (unfold cs_dependents_def children_def child_def, auto simp:eq_depend)
+ − 535
qed
+ − 536
qed
+ − 537
next
+ − 538
show "?f ` dependents (wq s) th
+ − 539
\<subseteq> \<Union>{?f ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ − 540
proof
+ − 541
fix x
+ − 542
assume x_in: "x \<in> (\<lambda>th. preced th s) ` dependents (wq s) th"
+ − 543
then obtain th' where
+ − 544
eq_x: "x = ?f th'" and dp: "(Th th', Th th) \<in> (depend s)^+"
+ − 545
by (auto simp:cs_dependents_def eq_depend)
+ − 546
from depend_children[OF dp]
+ − 547
have "th' \<in> children s th \<or> (\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+)" .
+ − 548
thus "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ − 549
proof
+ − 550
assume "th' \<in> children s th"
+ − 551
with eq_x
+ − 552
show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ − 553
by auto
+ − 554
next
+ − 555
assume "\<exists>th3. th3 \<in> children s th \<and> (Th th', Th th3) \<in> (depend s)\<^sup>+"
+ − 556
then obtain th3 where th3_in: "th3 \<in> children s th"
+ − 557
and dp3: "(Th th', Th th3) \<in> (depend s)\<^sup>+" by auto
+ − 558
show "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"
+ − 559
proof -
+ − 560
from dp3
+ − 561
have "th' \<in> dependents (wq s) th3"
+ − 562
by (auto simp:cs_dependents_def eq_depend)
+ − 563
with eq_x th3_in show ?thesis by auto
+ − 564
qed
+ − 565
qed
+ − 566
qed
+ − 567
qed
+ − 568
thus ?thesis by simp
+ − 569
qed
+ − 570
finally have "Max ((\<lambda>th. preced th s) ` dependents (wq s) th) = Max (?L)"
+ − 571
(is "?X = ?Y") by auto
+ − 572
moreover have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
+ − 573
max (?f th) ?X"
+ − 574
proof -
+ − 575
have "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
+ − 576
Max ({?f th} \<union> ?f ` (dependents (wq s) th))" by simp
+ − 577
also have "\<dots> = max (Max {?f th}) (Max (?f ` (dependents (wq s) th)))"
+ − 578
proof(rule Max_Un, auto)
+ − 579
from finite_threads[OF vt] and dependents_threads[OF vt, of th]
+ − 580
show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th)" by (auto simp:finite_subset)
+ − 581
next
+ − 582
assume "dependents (wq s) th = {}"
+ − 583
with False and children_dependents show False by auto
+ − 584
qed
+ − 585
also have "\<dots> = max (?f th) ?X" by simp
+ − 586
finally show ?thesis .
+ − 587
qed
+ − 588
moreover have "Max ({preced th s} \<union>
+ − 589
(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) =
+ − 590
max (?f th) ?Y"
+ − 591
proof -
+ − 592
have "Max ({preced th s} \<union>
+ − 593
(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th) =
+ − 594
max (Max {preced th s}) ?Y"
+ − 595
proof(rule Max_Un, auto)
+ − 596
from finite_threads[OF vt] dependents_threads[OF vt, of th] children_dependents [of s th]
+ − 597
show "finite ((\<lambda>th. Max (insert (preced th s) ((\<lambda>th. preced th s) ` dependents (wq s) th))) `
+ − 598
children s th)"
+ − 599
by (auto simp:finite_subset)
+ − 600
next
+ − 601
assume "children s th = {}"
+ − 602
with False show False by auto
+ − 603
qed
+ − 604
thus ?thesis by simp
+ − 605
qed
+ − 606
ultimately show ?thesis by auto
+ − 607
next
+ − 608
case True
+ − 609
moreover have "dependents (wq s) th = {}"
+ − 610
proof -
+ − 611
{ fix th'
+ − 612
assume "th' \<in> dependents (wq s) th"
+ − 613
hence " (Th th', Th th) \<in> (depend s)\<^sup>+" by (simp add:cs_dependents_def eq_depend)
+ − 614
from depend_children[OF this] and True
+ − 615
have "False" by auto
+ − 616
} thus ?thesis by auto
+ − 617
qed
+ − 618
ultimately show ?thesis by auto
+ − 619
qed
+ − 620
qed
+ − 621
+ − 622
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
+ − 623
where "cps s = {(th, cp s th) | th . th \<in> threads s}"
+ − 624
+ − 625
locale step_set_cps =
+ − 626
fixes s' th prio s
+ − 627
defines s_def : "s \<equiv> (Set th prio#s')"
+ − 628
assumes vt_s: "vt step s"
+ − 629
+ − 630
context step_set_cps
+ − 631
begin
+ − 632
+ − 633
lemma eq_preced:
+ − 634
fixes th'
+ − 635
assumes "th' \<noteq> th"
+ − 636
shows "preced th' s = preced th' s'"
+ − 637
proof -
+ − 638
from assms show ?thesis
+ − 639
by (unfold s_def, auto simp:preced_def)
+ − 640
qed
+ − 641
+ − 642
lemma eq_dep: "depend s = depend s'"
+ − 643
by (unfold s_def depend_set_unchanged, auto)
+ − 644
+ − 645
lemma eq_cp:
+ − 646
fixes th'
+ − 647
assumes neq_th: "th' \<noteq> th"
+ − 648
and nd: "th \<notin> dependents s th'"
+ − 649
shows "cp s th' = cp s' th'"
+ − 650
apply (unfold cp_eq_cpreced cpreced_def)
+ − 651
proof -
+ − 652
have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+ − 653
by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+ − 654
moreover {
+ − 655
fix th1
+ − 656
assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+ − 657
hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ − 658
hence "preced th1 s = preced th1 s'"
+ − 659
proof
+ − 660
assume "th1 = th'"
+ − 661
with eq_preced[OF neq_th]
+ − 662
show "preced th1 s = preced th1 s'" by simp
+ − 663
next
+ − 664
assume "th1 \<in> dependents (wq s') th'"
+ − 665
with nd and eq_dp have "th1 \<noteq> th"
+ − 666
by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
+ − 667
from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp
+ − 668
qed
+ − 669
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 670
((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ − 671
by (auto simp:image_def)
+ − 672
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 673
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ − 674
qed
+ − 675
+ − 676
lemma eq_up:
+ − 677
fixes th' th''
+ − 678
assumes dp1: "th \<in> dependents s th'"
+ − 679
and dp2: "th' \<in> dependents s th''"
+ − 680
and eq_cps: "cp s th' = cp s' th'"
+ − 681
shows "cp s th'' = cp s' th''"
+ − 682
proof -
+ − 683
from dp2
+ − 684
have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+ − 685
from depend_child[OF vt_s this[unfolded eq_depend]]
+ − 686
have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
+ − 687
moreover { fix n th''
+ − 688
have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
+ − 689
(\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
+ − 690
proof(erule trancl_induct, auto)
+ − 691
fix y th''
+ − 692
assume y_ch: "(y, Th th'') \<in> child s"
+ − 693
and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
+ − 694
and ch': "(Th th', y) \<in> (child s)\<^sup>+"
+ − 695
from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
+ − 696
with ih have eq_cpy:"cp s thy = cp s' thy" by blast
+ − 697
from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+ − 698
moreover from child_depend_p[OF ch'] and eq_y
+ − 699
have "(Th th', Th thy) \<in> (depend s)^+" by simp
+ − 700
ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
+ − 701
show "cp s th'' = cp s' th''"
+ − 702
apply (subst cp_rec[OF vt_s])
+ − 703
proof -
+ − 704
have "preced th'' s = preced th'' s'"
+ − 705
proof(rule eq_preced)
+ − 706
show "th'' \<noteq> th"
+ − 707
proof
+ − 708
assume "th'' = th"
+ − 709
with dp_thy y_ch[unfolded eq_y]
+ − 710
have "(Th th, Th th) \<in> (depend s)^+"
+ − 711
by (auto simp:child_def)
+ − 712
with wf_trancl[OF wf_depend[OF vt_s]]
+ − 713
show False by auto
+ − 714
qed
+ − 715
qed
+ − 716
moreover {
+ − 717
fix th1
+ − 718
assume th1_in: "th1 \<in> children s th''"
+ − 719
have "cp s th1 = cp s' th1"
+ − 720
proof(cases "th1 = thy")
+ − 721
case True
+ − 722
with eq_cpy show ?thesis by simp
+ − 723
next
+ − 724
case False
+ − 725
have neq_th1: "th1 \<noteq> th"
+ − 726
proof
+ − 727
assume eq_th1: "th1 = th"
+ − 728
with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
+ − 729
from children_no_dep[OF vt_s _ _ this] and
+ − 730
th1_in y_ch eq_y show False by (auto simp:children_def)
+ − 731
qed
+ − 732
have "th \<notin> dependents s th1"
+ − 733
proof
+ − 734
assume h:"th \<in> dependents s th1"
+ − 735
from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
+ − 736
from dependents_child_unique[OF vt_s _ _ h this]
+ − 737
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
+ − 738
with False show False by auto
+ − 739
qed
+ − 740
from eq_cp[OF neq_th1 this]
+ − 741
show ?thesis .
+ − 742
qed
+ − 743
}
+ − 744
ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
+ − 745
{preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
+ − 746
moreover have "children s th'' = children s' th''"
+ − 747
by (unfold children_def child_def s_def depend_set_unchanged, simp)
+ − 748
ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
+ − 749
by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
+ − 750
qed
+ − 751
next
+ − 752
fix th''
+ − 753
assume dp': "(Th th', Th th'') \<in> child s"
+ − 754
show "cp s th'' = cp s' th''"
+ − 755
apply (subst cp_rec[OF vt_s])
+ − 756
proof -
+ − 757
have "preced th'' s = preced th'' s'"
+ − 758
proof(rule eq_preced)
+ − 759
show "th'' \<noteq> th"
+ − 760
proof
+ − 761
assume "th'' = th"
+ − 762
with dp1 dp'
+ − 763
have "(Th th, Th th) \<in> (depend s)^+"
+ − 764
by (auto simp:child_def s_dependents_def eq_depend)
+ − 765
with wf_trancl[OF wf_depend[OF vt_s]]
+ − 766
show False by auto
+ − 767
qed
+ − 768
qed
+ − 769
moreover {
+ − 770
fix th1
+ − 771
assume th1_in: "th1 \<in> children s th''"
+ − 772
have "cp s th1 = cp s' th1"
+ − 773
proof(cases "th1 = th'")
+ − 774
case True
+ − 775
with eq_cps show ?thesis by simp
+ − 776
next
+ − 777
case False
+ − 778
have neq_th1: "th1 \<noteq> th"
+ − 779
proof
+ − 780
assume eq_th1: "th1 = th"
+ − 781
with dp1 have "(Th th1, Th th') \<in> (depend s)^+"
+ − 782
by (auto simp:s_dependents_def eq_depend)
+ − 783
from children_no_dep[OF vt_s _ _ this]
+ − 784
th1_in dp'
+ − 785
show False by (auto simp:children_def)
+ − 786
qed
+ − 787
thus ?thesis
+ − 788
proof(rule eq_cp)
+ − 789
show "th \<notin> dependents s th1"
+ − 790
proof
+ − 791
assume "th \<in> dependents s th1"
+ − 792
from dependents_child_unique[OF vt_s _ _ this dp1]
+ − 793
th1_in dp' have "th1 = th'"
+ − 794
by (auto simp:children_def)
+ − 795
with False show False by auto
+ − 796
qed
+ − 797
qed
+ − 798
qed
+ − 799
}
+ − 800
ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
+ − 801
{preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
+ − 802
moreover have "children s th'' = children s' th''"
+ − 803
by (unfold children_def child_def s_def depend_set_unchanged, simp)
+ − 804
ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
+ − 805
by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
+ − 806
qed
+ − 807
qed
+ − 808
}
+ − 809
ultimately show ?thesis by auto
+ − 810
qed
+ − 811
+ − 812
lemma eq_up_self:
+ − 813
fixes th' th''
+ − 814
assumes dp: "th \<in> dependents s th''"
+ − 815
and eq_cps: "cp s th = cp s' th"
+ − 816
shows "cp s th'' = cp s' th''"
+ − 817
proof -
+ − 818
from dp
+ − 819
have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+ − 820
from depend_child[OF vt_s this[unfolded eq_depend]]
+ − 821
have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .
+ − 822
moreover { fix n th''
+ − 823
have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
+ − 824
(\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
+ − 825
proof(erule trancl_induct, auto)
+ − 826
fix y th''
+ − 827
assume y_ch: "(y, Th th'') \<in> child s"
+ − 828
and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
+ − 829
and ch': "(Th th, y) \<in> (child s)\<^sup>+"
+ − 830
from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
+ − 831
with ih have eq_cpy:"cp s thy = cp s' thy" by blast
+ − 832
from child_depend_p[OF ch'] and eq_y
+ − 833
have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by simp
+ − 834
show "cp s th'' = cp s' th''"
+ − 835
apply (subst cp_rec[OF vt_s])
+ − 836
proof -
+ − 837
have "preced th'' s = preced th'' s'"
+ − 838
proof(rule eq_preced)
+ − 839
show "th'' \<noteq> th"
+ − 840
proof
+ − 841
assume "th'' = th"
+ − 842
with dp_thy y_ch[unfolded eq_y]
+ − 843
have "(Th th, Th th) \<in> (depend s)^+"
+ − 844
by (auto simp:child_def)
+ − 845
with wf_trancl[OF wf_depend[OF vt_s]]
+ − 846
show False by auto
+ − 847
qed
+ − 848
qed
+ − 849
moreover {
+ − 850
fix th1
+ − 851
assume th1_in: "th1 \<in> children s th''"
+ − 852
have "cp s th1 = cp s' th1"
+ − 853
proof(cases "th1 = thy")
+ − 854
case True
+ − 855
with eq_cpy show ?thesis by simp
+ − 856
next
+ − 857
case False
+ − 858
have neq_th1: "th1 \<noteq> th"
+ − 859
proof
+ − 860
assume eq_th1: "th1 = th"
+ − 861
with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
+ − 862
from children_no_dep[OF vt_s _ _ this] and
+ − 863
th1_in y_ch eq_y show False by (auto simp:children_def)
+ − 864
qed
+ − 865
have "th \<notin> dependents s th1"
+ − 866
proof
+ − 867
assume h:"th \<in> dependents s th1"
+ − 868
from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
+ − 869
from dependents_child_unique[OF vt_s _ _ h this]
+ − 870
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
+ − 871
with False show False by auto
+ − 872
qed
+ − 873
from eq_cp[OF neq_th1 this]
+ − 874
show ?thesis .
+ − 875
qed
+ − 876
}
+ − 877
ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
+ − 878
{preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
+ − 879
moreover have "children s th'' = children s' th''"
+ − 880
by (unfold children_def child_def s_def depend_set_unchanged, simp)
+ − 881
ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
+ − 882
by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
+ − 883
qed
+ − 884
next
+ − 885
fix th''
+ − 886
assume dp': "(Th th, Th th'') \<in> child s"
+ − 887
show "cp s th'' = cp s' th''"
+ − 888
apply (subst cp_rec[OF vt_s])
+ − 889
proof -
+ − 890
have "preced th'' s = preced th'' s'"
+ − 891
proof(rule eq_preced)
+ − 892
show "th'' \<noteq> th"
+ − 893
proof
+ − 894
assume "th'' = th"
+ − 895
with dp dp'
+ − 896
have "(Th th, Th th) \<in> (depend s)^+"
+ − 897
by (auto simp:child_def s_dependents_def eq_depend)
+ − 898
with wf_trancl[OF wf_depend[OF vt_s]]
+ − 899
show False by auto
+ − 900
qed
+ − 901
qed
+ − 902
moreover {
+ − 903
fix th1
+ − 904
assume th1_in: "th1 \<in> children s th''"
+ − 905
have "cp s th1 = cp s' th1"
+ − 906
proof(cases "th1 = th")
+ − 907
case True
+ − 908
with eq_cps show ?thesis by simp
+ − 909
next
+ − 910
case False
+ − 911
assume neq_th1: "th1 \<noteq> th"
+ − 912
thus ?thesis
+ − 913
proof(rule eq_cp)
+ − 914
show "th \<notin> dependents s th1"
+ − 915
proof
+ − 916
assume "th \<in> dependents s th1"
+ − 917
hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+ − 918
from children_no_dep[OF vt_s _ _ this]
+ − 919
and th1_in dp' show False
+ − 920
by (auto simp:children_def)
+ − 921
qed
+ − 922
qed
+ − 923
qed
+ − 924
}
+ − 925
ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
+ − 926
{preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
+ − 927
moreover have "children s th'' = children s' th''"
+ − 928
by (unfold children_def child_def s_def depend_set_unchanged, simp)
+ − 929
ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
+ − 930
by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
+ − 931
qed
+ − 932
qed
+ − 933
}
+ − 934
ultimately show ?thesis by auto
+ − 935
qed
+ − 936
end
+ − 937
+ − 938
lemma next_waiting:
+ − 939
assumes vt: "vt step s"
+ − 940
and nxt: "next_th s th cs th'"
+ − 941
shows "waiting s th' cs"
+ − 942
proof -
+ − 943
from assms show ?thesis
+ − 944
apply (auto simp:next_th_def s_waiting_def)
+ − 945
proof -
+ − 946
fix rest
+ − 947
assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
+ − 948
and eq_wq: "wq s cs = th # rest"
+ − 949
and ne: "rest \<noteq> []"
+ − 950
have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
+ − 951
proof(rule someI2)
+ − 952
from wq_distinct[OF vt, of cs] eq_wq
+ − 953
show "distinct rest \<and> set rest = set rest" by auto
+ − 954
next
+ − 955
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+ − 956
qed
+ − 957
with ni
+ − 958
have "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set (SOME q. distinct q \<and> set q = set rest)"
+ − 959
by simp
+ − 960
moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+ − 961
proof(rule someI2)
+ − 962
from wq_distinct[OF vt, of cs] eq_wq
+ − 963
show "distinct rest \<and> set rest = set rest" by auto
+ − 964
next
+ − 965
from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
+ − 966
qed
+ − 967
ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
+ − 968
next
+ − 969
fix rest
+ − 970
assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
+ − 971
and ne: "rest \<noteq> []"
+ − 972
have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
+ − 973
proof(rule someI2)
+ − 974
from wq_distinct[OF vt, of cs] eq_wq
+ − 975
show "distinct rest \<and> set rest = set rest" by auto
+ − 976
next
+ − 977
from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto
+ − 978
qed
+ − 979
hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"
+ − 980
by auto
+ − 981
moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
+ − 982
proof(rule someI2)
+ − 983
from wq_distinct[OF vt, of cs] eq_wq
+ − 984
show "distinct rest \<and> set rest = set rest" by auto
+ − 985
next
+ − 986
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
+ − 987
qed
+ − 988
ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp
+ − 989
with eq_wq and wq_distinct[OF vt, of cs]
+ − 990
show False by auto
+ − 991
qed
+ − 992
qed
+ − 993
+ − 994
locale step_v_cps =
+ − 995
fixes s' th cs s
+ − 996
defines s_def : "s \<equiv> (V th cs#s')"
+ − 997
assumes vt_s: "vt step s"
+ − 998
+ − 999
locale step_v_cps_nt = step_v_cps +
+ − 1000
fixes th'
+ − 1001
assumes nt: "next_th s' th cs th'"
+ − 1002
+ − 1003
context step_v_cps_nt
+ − 1004
begin
+ − 1005
+ − 1006
lemma depend_s:
+ − 1007
"depend s = (depend s' - {(Cs cs, Th th)} - {(Th th', Cs cs)}) \<union>
+ − 1008
{(Cs cs, Th th')}"
+ − 1009
proof -
+ − 1010
from step_depend_v[OF vt_s[unfolded s_def], folded s_def]
+ − 1011
and nt show ?thesis by (auto intro:next_th_unique)
+ − 1012
qed
+ − 1013
+ − 1014
lemma dependents_kept:
+ − 1015
fixes th''
+ − 1016
assumes neq1: "th'' \<noteq> th"
+ − 1017
and neq2: "th'' \<noteq> th'"
+ − 1018
shows "dependents (wq s) th'' = dependents (wq s') th''"
+ − 1019
proof(auto)
+ − 1020
fix x
+ − 1021
assume "x \<in> dependents (wq s) th''"
+ − 1022
hence dp: "(Th x, Th th'') \<in> (depend s)^+"
+ − 1023
by (auto simp:cs_dependents_def eq_depend)
+ − 1024
{ fix n
+ − 1025
have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow> (n, Th th'') \<in> (depend s')^+"
+ − 1026
proof(induct rule:converse_trancl_induct)
+ − 1027
fix y
+ − 1028
assume "(y, Th th'') \<in> depend s"
+ − 1029
with depend_s neq1 neq2
+ − 1030
have "(y, Th th'') \<in> depend s'" by auto
+ − 1031
thus "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
+ − 1032
next
+ − 1033
fix y z
+ − 1034
assume yz: "(y, z) \<in> depend s"
+ − 1035
and ztp: "(z, Th th'') \<in> (depend s)\<^sup>+"
+ − 1036
and ztp': "(z, Th th'') \<in> (depend s')\<^sup>+"
+ − 1037
have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
+ − 1038
proof
+ − 1039
show "y \<noteq> Cs cs"
+ − 1040
proof
+ − 1041
assume eq_y: "y = Cs cs"
+ − 1042
with yz have dp_yz: "(Cs cs, z) \<in> depend s" by simp
+ − 1043
from depend_s
+ − 1044
have cst': "(Cs cs, Th th') \<in> depend s" by simp
+ − 1045
from unique_depend[OF vt_s this dp_yz]
+ − 1046
have eq_z: "z = Th th'" by simp
+ − 1047
with ztp have "(Th th', Th th'') \<in> (depend s)^+" by simp
+ − 1048
from converse_tranclE[OF this]
+ − 1049
obtain cs' where dp'': "(Th th', Cs cs') \<in> depend s"
+ − 1050
by (auto simp:s_depend_def)
+ − 1051
with depend_s have dp': "(Th th', Cs cs') \<in> depend s'" by auto
+ − 1052
from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (depend s)^+" by auto
+ − 1053
moreover have "cs' = cs"
+ − 1054
proof -
+ − 1055
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
+ − 1056
have "(Th th', Cs cs) \<in> depend s'"
+ − 1057
by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+ − 1058
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
+ − 1059
show ?thesis by simp
+ − 1060
qed
+ − 1061
ultimately have "(Cs cs, Cs cs) \<in> (depend s)^+" by simp
+ − 1062
moreover note wf_trancl[OF wf_depend[OF vt_s]]
+ − 1063
ultimately show False by auto
+ − 1064
qed
+ − 1065
next
+ − 1066
show "y \<noteq> Th th'"
+ − 1067
proof
+ − 1068
assume eq_y: "y = Th th'"
+ − 1069
with yz have dps: "(Th th', z) \<in> depend s" by simp
+ − 1070
with depend_s have dps': "(Th th', z) \<in> depend s'" by auto
+ − 1071
have "z = Cs cs"
+ − 1072
proof -
+ − 1073
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
+ − 1074
have "(Th th', Cs cs) \<in> depend s'"
+ − 1075
by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+ − 1076
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
+ − 1077
show ?thesis .
+ − 1078
qed
+ − 1079
with dps depend_s show False by auto
+ − 1080
qed
+ − 1081
qed
+ − 1082
with depend_s yz have "(y, z) \<in> depend s'" by auto
+ − 1083
with ztp'
+ − 1084
show "(y, Th th'') \<in> (depend s')\<^sup>+" by auto
+ − 1085
qed
+ − 1086
}
+ − 1087
from this[OF dp]
+ − 1088
show "x \<in> dependents (wq s') th''"
+ − 1089
by (auto simp:cs_dependents_def eq_depend)
+ − 1090
next
+ − 1091
fix x
+ − 1092
assume "x \<in> dependents (wq s') th''"
+ − 1093
hence dp: "(Th x, Th th'') \<in> (depend s')^+"
+ − 1094
by (auto simp:cs_dependents_def eq_depend)
+ − 1095
{ fix n
+ − 1096
have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow> (n, Th th'') \<in> (depend s)^+"
+ − 1097
proof(induct rule:converse_trancl_induct)
+ − 1098
fix y
+ − 1099
assume "(y, Th th'') \<in> depend s'"
+ − 1100
with depend_s neq1 neq2
+ − 1101
have "(y, Th th'') \<in> depend s" by auto
+ − 1102
thus "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
+ − 1103
next
+ − 1104
fix y z
+ − 1105
assume yz: "(y, z) \<in> depend s'"
+ − 1106
and ztp: "(z, Th th'') \<in> (depend s')\<^sup>+"
+ − 1107
and ztp': "(z, Th th'') \<in> (depend s)\<^sup>+"
+ − 1108
have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"
+ − 1109
proof
+ − 1110
show "y \<noteq> Cs cs"
+ − 1111
proof
+ − 1112
assume eq_y: "y = Cs cs"
+ − 1113
with yz have dp_yz: "(Cs cs, z) \<in> depend s'" by simp
+ − 1114
from this have eq_z: "z = Th th"
+ − 1115
proof -
+ − 1116
from step_back_step[OF vt_s[unfolded s_def]]
+ − 1117
have "(Cs cs, Th th) \<in> depend s'"
+ − 1118
by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+ − 1119
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
+ − 1120
show ?thesis by simp
+ − 1121
qed
+ − 1122
from converse_tranclE[OF ztp]
+ − 1123
obtain u where "(z, u) \<in> depend s'" by auto
+ − 1124
moreover
+ − 1125
from step_back_step[OF vt_s[unfolded s_def]]
+ − 1126
have "th \<in> readys s'" by (cases, simp add:runing_def)
+ − 1127
moreover note eq_z
+ − 1128
ultimately show False
+ − 1129
by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+ − 1130
qed
+ − 1131
next
+ − 1132
show "y \<noteq> Th th'"
+ − 1133
proof
+ − 1134
assume eq_y: "y = Th th'"
+ − 1135
with yz have dps: "(Th th', z) \<in> depend s'" by simp
+ − 1136
have "z = Cs cs"
+ − 1137
proof -
+ − 1138
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
+ − 1139
have "(Th th', Cs cs) \<in> depend s'"
+ − 1140
by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+ − 1141
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
+ − 1142
show ?thesis .
+ − 1143
qed
+ − 1144
with ztp have cs_i: "(Cs cs, Th th'') \<in> (depend s')\<^sup>+" by simp
+ − 1145
from step_back_step[OF vt_s[unfolded s_def]]
+ − 1146
have cs_th: "(Cs cs, Th th) \<in> depend s'"
+ − 1147
by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+ − 1148
have "(Cs cs, Th th'') \<notin> depend s'"
+ − 1149
proof
+ − 1150
assume "(Cs cs, Th th'') \<in> depend s'"
+ − 1151
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]
+ − 1152
and neq1 show "False" by simp
+ − 1153
qed
+ − 1154
with converse_tranclE[OF cs_i]
+ − 1155
obtain u where cu: "(Cs cs, u) \<in> depend s'"
+ − 1156
and u_t: "(u, Th th'') \<in> (depend s')\<^sup>+" by auto
+ − 1157
have "u = Th th"
+ − 1158
proof -
+ − 1159
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th]
+ − 1160
show ?thesis .
+ − 1161
qed
+ − 1162
with u_t have "(Th th, Th th'') \<in> (depend s')\<^sup>+" by simp
+ − 1163
from converse_tranclE[OF this]
+ − 1164
obtain v where "(Th th, v) \<in> (depend s')" by auto
+ − 1165
moreover from step_back_step[OF vt_s[unfolded s_def]]
+ − 1166
have "th \<in> readys s'" by (cases, simp add:runing_def)
+ − 1167
ultimately show False
+ − 1168
by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+ − 1169
qed
+ − 1170
qed
+ − 1171
with depend_s yz have "(y, z) \<in> depend s" by auto
+ − 1172
with ztp'
+ − 1173
show "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
+ − 1174
qed
+ − 1175
}
+ − 1176
from this[OF dp]
+ − 1177
show "x \<in> dependents (wq s) th''"
+ − 1178
by (auto simp:cs_dependents_def eq_depend)
+ − 1179
qed
+ − 1180
+ − 1181
lemma cp_kept:
+ − 1182
fixes th''
+ − 1183
assumes neq1: "th'' \<noteq> th"
+ − 1184
and neq2: "th'' \<noteq> th'"
+ − 1185
shows "cp s th'' = cp s' th''"
+ − 1186
proof -
+ − 1187
from dependents_kept[OF neq1 neq2]
+ − 1188
have "dependents (wq s) th'' = dependents (wq s') th''" .
+ − 1189
moreover {
+ − 1190
fix th1
+ − 1191
assume "th1 \<in> dependents (wq s) th''"
+ − 1192
have "preced th1 s = preced th1 s'"
+ − 1193
by (unfold s_def, auto simp:preced_def)
+ − 1194
}
+ − 1195
moreover have "preced th'' s = preced th'' s'"
+ − 1196
by (unfold s_def, auto simp:preced_def)
+ − 1197
ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependents (wq s) th'')) =
+ − 1198
((\<lambda>th. preced th s') ` ({th''} \<union> dependents (wq s') th''))"
+ − 1199
by (auto simp:image_def)
+ − 1200
thus ?thesis
+ − 1201
by (unfold cp_eq_cpreced cpreced_def, simp)
+ − 1202
qed
+ − 1203
+ − 1204
end
+ − 1205
+ − 1206
locale step_v_cps_nnt = step_v_cps +
+ − 1207
assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"
+ − 1208
+ − 1209
context step_v_cps_nnt
+ − 1210
begin
+ − 1211
+ − 1212
lemma nw_cs: "(Th th1, Cs cs) \<notin> depend s'"
+ − 1213
proof
+ − 1214
assume "(Th th1, Cs cs) \<in> depend s'"
+ − 1215
thus "False"
+ − 1216
apply (auto simp:s_depend_def cs_waiting_def)
+ − 1217
proof -
+ − 1218
assume h1: "th1 \<in> set (wq s' cs)"
+ − 1219
and h2: "th1 \<noteq> hd (wq s' cs)"
+ − 1220
from step_back_step[OF vt_s[unfolded s_def]]
+ − 1221
show "False"
+ − 1222
proof(cases)
+ − 1223
assume "holding s' th cs"
+ − 1224
then obtain rest where
+ − 1225
eq_wq: "wq s' cs = th#rest"
+ − 1226
apply (unfold s_holding_def)
+ − 1227
by (case_tac "(wq s' cs)", auto)
+ − 1228
with h1 h2 have ne: "rest \<noteq> []" by auto
+ − 1229
with eq_wq
+ − 1230
have "next_th s' th cs (hd (SOME q. distinct q \<and> set q = set rest))"
+ − 1231
by(unfold next_th_def, rule_tac x = "rest" in exI, auto)
+ − 1232
with nnt show ?thesis by auto
+ − 1233
qed
+ − 1234
qed
+ − 1235
qed
+ − 1236
+ − 1237
lemma depend_s: "depend s = depend s' - {(Cs cs, Th th)}"
+ − 1238
proof -
+ − 1239
from nnt and step_depend_v[OF vt_s[unfolded s_def], folded s_def]
+ − 1240
show ?thesis by auto
+ − 1241
qed
+ − 1242
+ − 1243
lemma child_kept_left:
+ − 1244
assumes
+ − 1245
"(n1, n2) \<in> (child s')^+"
+ − 1246
shows "(n1, n2) \<in> (child s)^+"
+ − 1247
proof -
+ − 1248
from assms show ?thesis
+ − 1249
proof(induct rule: converse_trancl_induct)
+ − 1250
case (base y)
+ − 1251
from base obtain th1 cs1 th2
+ − 1252
where h1: "(Th th1, Cs cs1) \<in> depend s'"
+ − 1253
and h2: "(Cs cs1, Th th2) \<in> depend s'"
+ − 1254
and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def)
+ − 1255
have "cs1 \<noteq> cs"
+ − 1256
proof
+ − 1257
assume eq_cs: "cs1 = cs"
+ − 1258
with h1 have "(Th th1, Cs cs1) \<in> depend s'" by simp
+ − 1259
with nw_cs eq_cs show False by auto
+ − 1260
qed
+ − 1261
with h1 h2 depend_s have
+ − 1262
h1': "(Th th1, Cs cs1) \<in> depend s" and
+ − 1263
h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+ − 1264
hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
+ − 1265
with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
+ − 1266
thus ?case by auto
+ − 1267
next
+ − 1268
case (step y z)
+ − 1269
have "(y, z) \<in> child s'" by fact
+ − 1270
then obtain th1 cs1 th2
+ − 1271
where h1: "(Th th1, Cs cs1) \<in> depend s'"
+ − 1272
and h2: "(Cs cs1, Th th2) \<in> depend s'"
+ − 1273
and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def)
+ − 1274
have "cs1 \<noteq> cs"
+ − 1275
proof
+ − 1276
assume eq_cs: "cs1 = cs"
+ − 1277
with h1 have "(Th th1, Cs cs1) \<in> depend s'" by simp
+ − 1278
with nw_cs eq_cs show False by auto
+ − 1279
qed
+ − 1280
with h1 h2 depend_s have
+ − 1281
h1': "(Th th1, Cs cs1) \<in> depend s" and
+ − 1282
h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+ − 1283
hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
+ − 1284
with eq_y eq_z have "(y, z) \<in> child s" by simp
+ − 1285
moreover have "(z, n2) \<in> (child s)^+" by fact
+ − 1286
ultimately show ?case by auto
+ − 1287
qed
+ − 1288
qed
+ − 1289
+ − 1290
lemma child_kept_right:
+ − 1291
assumes
+ − 1292
"(n1, n2) \<in> (child s)^+"
+ − 1293
shows "(n1, n2) \<in> (child s')^+"
+ − 1294
proof -
+ − 1295
from assms show ?thesis
+ − 1296
proof(induct)
+ − 1297
case (base y)
+ − 1298
from base and depend_s
+ − 1299
have "(n1, y) \<in> child s'"
+ − 1300
by (auto simp:child_def)
+ − 1301
thus ?case by auto
+ − 1302
next
+ − 1303
case (step y z)
+ − 1304
have "(y, z) \<in> child s" by fact
+ − 1305
with depend_s have "(y, z) \<in> child s'"
+ − 1306
by (auto simp:child_def)
+ − 1307
moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
+ − 1308
ultimately show ?case by auto
+ − 1309
qed
+ − 1310
qed
+ − 1311
+ − 1312
lemma eq_child: "(child s)^+ = (child s')^+"
+ − 1313
by (insert child_kept_left child_kept_right, auto)
+ − 1314
+ − 1315
lemma eq_cp:
+ − 1316
fixes th'
+ − 1317
shows "cp s th' = cp s' th'"
+ − 1318
apply (unfold cp_eq_cpreced cpreced_def)
+ − 1319
proof -
+ − 1320
have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+ − 1321
apply (unfold cs_dependents_def, unfold eq_depend)
+ − 1322
proof -
+ − 1323
from eq_child
+ − 1324
have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
+ − 1325
by simp
+ − 1326
with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+ − 1327
show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
+ − 1328
by simp
+ − 1329
qed
+ − 1330
moreover {
+ − 1331
fix th1
+ − 1332
assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+ − 1333
hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ − 1334
hence "preced th1 s = preced th1 s'"
+ − 1335
proof
+ − 1336
assume "th1 = th'"
+ − 1337
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+ − 1338
next
+ − 1339
assume "th1 \<in> dependents (wq s') th'"
+ − 1340
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+ − 1341
qed
+ − 1342
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1343
((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ − 1344
by (auto simp:image_def)
+ − 1345
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1346
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ − 1347
qed
+ − 1348
+ − 1349
end
+ − 1350
+ − 1351
locale step_P_cps =
+ − 1352
fixes s' th cs s
+ − 1353
defines s_def : "s \<equiv> (P th cs#s')"
+ − 1354
assumes vt_s: "vt step s"
+ − 1355
+ − 1356
locale step_P_cps_ne =step_P_cps +
+ − 1357
assumes ne: "wq s' cs \<noteq> []"
+ − 1358
272
+ − 1359
locale step_P_cps_e =step_P_cps +
+ − 1360
assumes ee: "wq s' cs = []"
+ − 1361
+ − 1362
context step_P_cps_e
+ − 1363
begin
+ − 1364
+ − 1365
lemma depend_s: "depend s = depend s' \<union> {(Cs cs, Th th)}"
+ − 1366
proof -
+ − 1367
from ee and step_depend_p[OF vt_s[unfolded s_def], folded s_def]
+ − 1368
show ?thesis by auto
+ − 1369
qed
+ − 1370
+ − 1371
lemma child_kept_left:
+ − 1372
assumes
+ − 1373
"(n1, n2) \<in> (child s')^+"
+ − 1374
shows "(n1, n2) \<in> (child s)^+"
+ − 1375
proof -
+ − 1376
from assms show ?thesis
+ − 1377
proof(induct rule: converse_trancl_induct)
+ − 1378
case (base y)
+ − 1379
from base obtain th1 cs1 th2
+ − 1380
where h1: "(Th th1, Cs cs1) \<in> depend s'"
+ − 1381
and h2: "(Cs cs1, Th th2) \<in> depend s'"
+ − 1382
and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2" by (auto simp:child_def)
+ − 1383
have "cs1 \<noteq> cs"
+ − 1384
proof
+ − 1385
assume eq_cs: "cs1 = cs"
+ − 1386
with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp
+ − 1387
with ee show False
+ − 1388
by (auto simp:s_depend_def cs_waiting_def)
+ − 1389
qed
+ − 1390
with h1 h2 depend_s have
+ − 1391
h1': "(Th th1, Cs cs1) \<in> depend s" and
+ − 1392
h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+ − 1393
hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
+ − 1394
with eq_y eq_n2 have "(y, n2) \<in> child s" by simp
+ − 1395
thus ?case by auto
+ − 1396
next
+ − 1397
case (step y z)
+ − 1398
have "(y, z) \<in> child s'" by fact
+ − 1399
then obtain th1 cs1 th2
+ − 1400
where h1: "(Th th1, Cs cs1) \<in> depend s'"
+ − 1401
and h2: "(Cs cs1, Th th2) \<in> depend s'"
+ − 1402
and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def)
+ − 1403
have "cs1 \<noteq> cs"
+ − 1404
proof
+ − 1405
assume eq_cs: "cs1 = cs"
+ − 1406
with h1 have "(Th th1, Cs cs) \<in> depend s'" by simp
+ − 1407
with ee show False
+ − 1408
by (auto simp:s_depend_def cs_waiting_def)
+ − 1409
qed
+ − 1410
with h1 h2 depend_s have
+ − 1411
h1': "(Th th1, Cs cs1) \<in> depend s" and
+ − 1412
h2': "(Cs cs1, Th th2) \<in> depend s" by auto
+ − 1413
hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)
+ − 1414
with eq_y eq_z have "(y, z) \<in> child s" by simp
+ − 1415
moreover have "(z, n2) \<in> (child s)^+" by fact
+ − 1416
ultimately show ?case by auto
+ − 1417
qed
+ − 1418
qed
+ − 1419
+ − 1420
lemma child_kept_right:
+ − 1421
assumes
+ − 1422
"(n1, n2) \<in> (child s)^+"
+ − 1423
shows "(n1, n2) \<in> (child s')^+"
+ − 1424
proof -
+ − 1425
from assms show ?thesis
+ − 1426
proof(induct)
+ − 1427
case (base y)
+ − 1428
from base and depend_s
+ − 1429
have "(n1, y) \<in> child s'"
+ − 1430
apply (auto simp:child_def)
+ − 1431
proof -
+ − 1432
fix th'
+ − 1433
assume "(Th th', Cs cs) \<in> depend s'"
+ − 1434
with ee have "False"
+ − 1435
by (auto simp:s_depend_def cs_waiting_def)
+ − 1436
thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto
+ − 1437
qed
+ − 1438
thus ?case by auto
+ − 1439
next
+ − 1440
case (step y z)
+ − 1441
have "(y, z) \<in> child s" by fact
+ − 1442
with depend_s have "(y, z) \<in> child s'"
+ − 1443
apply (auto simp:child_def)
+ − 1444
proof -
+ − 1445
fix th'
+ − 1446
assume "(Th th', Cs cs) \<in> depend s'"
+ − 1447
with ee have "False"
+ − 1448
by (auto simp:s_depend_def cs_waiting_def)
+ − 1449
thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto
+ − 1450
qed
+ − 1451
moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact
+ − 1452
ultimately show ?case by auto
+ − 1453
qed
+ − 1454
qed
+ − 1455
+ − 1456
lemma eq_child: "(child s)^+ = (child s')^+"
+ − 1457
by (insert child_kept_left child_kept_right, auto)
+ − 1458
+ − 1459
lemma eq_cp:
+ − 1460
fixes th'
+ − 1461
shows "cp s th' = cp s' th'"
+ − 1462
apply (unfold cp_eq_cpreced cpreced_def)
+ − 1463
proof -
+ − 1464
have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+ − 1465
apply (unfold cs_dependents_def, unfold eq_depend)
+ − 1466
proof -
+ − 1467
from eq_child
+ − 1468
have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"
+ − 1469
by auto
+ − 1470
with child_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+ − 1471
show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend s')\<^sup>+}"
+ − 1472
by simp
+ − 1473
qed
+ − 1474
moreover {
+ − 1475
fix th1
+ − 1476
assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+ − 1477
hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ − 1478
hence "preced th1 s = preced th1 s'"
+ − 1479
proof
+ − 1480
assume "th1 = th'"
+ − 1481
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+ − 1482
next
+ − 1483
assume "th1 \<in> dependents (wq s') th'"
+ − 1484
show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+ − 1485
qed
+ − 1486
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1487
((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ − 1488
by (auto simp:image_def)
+ − 1489
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1490
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ − 1491
qed
+ − 1492
+ − 1493
end
+ − 1494
262
+ − 1495
context step_P_cps_ne
+ − 1496
begin
+ − 1497
+ − 1498
lemma depend_s: "depend s = depend s' \<union> {(Th th, Cs cs)}"
+ − 1499
proof -
+ − 1500
from step_depend_p[OF vt_s[unfolded s_def]] and ne
+ − 1501
show ?thesis by (simp add:s_def)
+ − 1502
qed
+ − 1503
+ − 1504
lemma eq_child_left:
+ − 1505
assumes nd: "(Th th, Th th') \<notin> (child s)^+"
+ − 1506
shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"
+ − 1507
proof(induct rule:converse_trancl_induct)
+ − 1508
case (base y)
+ − 1509
from base obtain th1 cs1
+ − 1510
where h1: "(Th th1, Cs cs1) \<in> depend s"
+ − 1511
and h2: "(Cs cs1, Th th') \<in> depend s"
+ − 1512
and eq_y: "y = Th th1" by (auto simp:child_def)
+ − 1513
have "th1 \<noteq> th"
+ − 1514
proof
+ − 1515
assume "th1 = th"
+ − 1516
with base eq_y have "(Th th, Th th') \<in> child s" by simp
+ − 1517
with nd show False by auto
+ − 1518
qed
+ − 1519
with h1 h2 depend_s
+ − 1520
have h1': "(Th th1, Cs cs1) \<in> depend s'" and
+ − 1521
h2': "(Cs cs1, Th th') \<in> depend s'" by auto
+ − 1522
with eq_y show ?case by (auto simp:child_def)
+ − 1523
next
+ − 1524
case (step y z)
+ − 1525
have yz: "(y, z) \<in> child s" by fact
+ − 1526
then obtain th1 cs1 th2
+ − 1527
where h1: "(Th th1, Cs cs1) \<in> depend s"
+ − 1528
and h2: "(Cs cs1, Th th2) \<in> depend s"
+ − 1529
and eq_y: "y = Th th1" and eq_z: "z = Th th2" by (auto simp:child_def)
+ − 1530
have "th1 \<noteq> th"
+ − 1531
proof
+ − 1532
assume "th1 = th"
+ − 1533
with yz eq_y have "(Th th, z) \<in> child s" by simp
+ − 1534
moreover have "(z, Th th') \<in> (child s)^+" by fact
+ − 1535
ultimately have "(Th th, Th th') \<in> (child s)^+" by auto
+ − 1536
with nd show False by auto
+ − 1537
qed
+ − 1538
with h1 h2 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s'"
+ − 1539
and h2': "(Cs cs1, Th th2) \<in> depend s'" by auto
+ − 1540
with eq_y eq_z have "(y, z) \<in> child s'" by (auto simp:child_def)
+ − 1541
moreover have "(z, Th th') \<in> (child s')^+" by fact
+ − 1542
ultimately show ?case by auto
+ − 1543
qed
+ − 1544
+ − 1545
lemma eq_child_right:
+ − 1546
shows "(n1, Th th') \<in> (child s')^+ \<Longrightarrow> (n1, Th th') \<in> (child s)^+"
+ − 1547
proof(induct rule:converse_trancl_induct)
+ − 1548
case (base y)
+ − 1549
with depend_s show ?case by (auto simp:child_def)
+ − 1550
next
+ − 1551
case (step y z)
+ − 1552
have "(y, z) \<in> child s'" by fact
+ − 1553
with depend_s have "(y, z) \<in> child s" by (auto simp:child_def)
+ − 1554
moreover have "(z, Th th') \<in> (child s)^+" by fact
+ − 1555
ultimately show ?case by auto
+ − 1556
qed
+ − 1557
+ − 1558
lemma eq_child:
+ − 1559
assumes nd: "(Th th, Th th') \<notin> (child s)^+"
+ − 1560
shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"
+ − 1561
by (insert eq_child_left[OF nd] eq_child_right, auto)
+ − 1562
+ − 1563
lemma eq_cp:
+ − 1564
fixes th'
+ − 1565
assumes nd: "th \<notin> dependents s th'"
+ − 1566
shows "cp s th' = cp s' th'"
+ − 1567
apply (unfold cp_eq_cpreced cpreced_def)
+ − 1568
proof -
+ − 1569
have nd': "(Th th, Th th') \<notin> (child s)^+"
+ − 1570
proof
+ − 1571
assume "(Th th, Th th') \<in> (child s)\<^sup>+"
+ − 1572
with child_depend_eq[OF vt_s]
+ − 1573
have "(Th th, Th th') \<in> (depend s)\<^sup>+" by simp
+ − 1574
with nd show False
+ − 1575
by (simp add:s_dependents_def eq_depend)
+ − 1576
qed
+ − 1577
have eq_dp: "dependents (wq s) th' = dependents (wq s') th'"
+ − 1578
proof(auto)
+ − 1579
fix x assume " x \<in> dependents (wq s) th'"
+ − 1580
thus "x \<in> dependents (wq s') th'"
+ − 1581
apply (auto simp:cs_dependents_def eq_depend)
+ − 1582
proof -
+ − 1583
assume "(Th x, Th th') \<in> (depend s)\<^sup>+"
+ − 1584
with child_depend_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp
+ − 1585
with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s')^+" by simp
+ − 1586
with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+ − 1587
show "(Th x, Th th') \<in> (depend s')\<^sup>+" by simp
+ − 1588
qed
+ − 1589
next
+ − 1590
fix x assume "x \<in> dependents (wq s') th'"
+ − 1591
thus "x \<in> dependents (wq s) th'"
+ − 1592
apply (auto simp:cs_dependents_def eq_depend)
+ − 1593
proof -
+ − 1594
assume "(Th x, Th th') \<in> (depend s')\<^sup>+"
+ − 1595
with child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]
+ − 1596
have "(Th x, Th th') \<in> (child s')\<^sup>+" by simp
+ − 1597
with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s)^+" by simp
+ − 1598
with child_depend_eq[OF vt_s]
+ − 1599
show "(Th x, Th th') \<in> (depend s)\<^sup>+" by simp
+ − 1600
qed
+ − 1601
qed
+ − 1602
moreover {
+ − 1603
fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)
+ − 1604
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1605
((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ − 1606
by (auto simp:image_def)
+ − 1607
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1608
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ − 1609
qed
+ − 1610
+ − 1611
lemma eq_up:
+ − 1612
fixes th' th''
+ − 1613
assumes dp1: "th \<in> dependents s th'"
+ − 1614
and dp2: "th' \<in> dependents s th''"
+ − 1615
and eq_cps: "cp s th' = cp s' th'"
+ − 1616
shows "cp s th'' = cp s' th''"
+ − 1617
proof -
+ − 1618
from dp2
+ − 1619
have "(Th th', Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependents_def)
+ − 1620
from depend_child[OF vt_s this[unfolded eq_depend]]
+ − 1621
have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
+ − 1622
moreover {
+ − 1623
fix n th''
+ − 1624
have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
+ − 1625
(\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
+ − 1626
proof(erule trancl_induct, auto)
+ − 1627
fix y th''
+ − 1628
assume y_ch: "(y, Th th'') \<in> child s"
+ − 1629
and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
+ − 1630
and ch': "(Th th', y) \<in> (child s)\<^sup>+"
+ − 1631
from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
+ − 1632
with ih have eq_cpy:"cp s thy = cp s' thy" by blast
+ − 1633
from dp1 have "(Th th, Th th') \<in> (depend s)^+" by (auto simp:s_dependents_def eq_depend)
+ − 1634
moreover from child_depend_p[OF ch'] and eq_y
+ − 1635
have "(Th th', Th thy) \<in> (depend s)^+" by simp
+ − 1636
ultimately have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by auto
+ − 1637
show "cp s th'' = cp s' th''"
+ − 1638
apply (subst cp_rec[OF vt_s])
+ − 1639
proof -
+ − 1640
have "preced th'' s = preced th'' s'"
+ − 1641
by (simp add:s_def preced_def)
+ − 1642
moreover {
+ − 1643
fix th1
+ − 1644
assume th1_in: "th1 \<in> children s th''"
+ − 1645
have "cp s th1 = cp s' th1"
+ − 1646
proof(cases "th1 = thy")
+ − 1647
case True
+ − 1648
with eq_cpy show ?thesis by simp
+ − 1649
next
+ − 1650
case False
+ − 1651
have neq_th1: "th1 \<noteq> th"
+ − 1652
proof
+ − 1653
assume eq_th1: "th1 = th"
+ − 1654
with dp_thy have "(Th th1, Th thy) \<in> (depend s)^+" by simp
+ − 1655
from children_no_dep[OF vt_s _ _ this] and
+ − 1656
th1_in y_ch eq_y show False by (auto simp:children_def)
+ − 1657
qed
+ − 1658
have "th \<notin> dependents s th1"
+ − 1659
proof
+ − 1660
assume h:"th \<in> dependents s th1"
+ − 1661
from eq_y dp_thy have "th \<in> dependents s thy" by (auto simp:s_dependents_def eq_depend)
+ − 1662
from dependents_child_unique[OF vt_s _ _ h this]
+ − 1663
th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
+ − 1664
with False show False by auto
+ − 1665
qed
+ − 1666
from eq_cp[OF this]
+ − 1667
show ?thesis .
+ − 1668
qed
+ − 1669
}
+ − 1670
ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
+ − 1671
{preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
+ − 1672
moreover have "children s th'' = children s' th''"
+ − 1673
apply (unfold children_def child_def s_def depend_set_unchanged, simp)
+ − 1674
apply (fold s_def, auto simp:depend_s)
+ − 1675
proof -
+ − 1676
assume "(Cs cs, Th th'') \<in> depend s'"
+ − 1677
with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
+ − 1678
from dp1 have "(Th th, Th th') \<in> (depend s)^+"
+ − 1679
by (auto simp:s_dependents_def eq_depend)
+ − 1680
from converse_tranclE[OF this]
+ − 1681
obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
+ − 1682
and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
+ − 1683
by (auto simp:s_depend_def)
+ − 1684
have eq_cs: "cs1 = cs"
+ − 1685
proof -
+ − 1686
from depend_s have "(Th th, Cs cs) \<in> depend s" by simp
+ − 1687
from unique_depend[OF vt_s this h1]
+ − 1688
show ?thesis by simp
+ − 1689
qed
+ − 1690
have False
+ − 1691
proof(rule converse_tranclE[OF h2])
+ − 1692
assume "(Cs cs1, Th th') \<in> depend s"
+ − 1693
with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp
+ − 1694
from unique_depend[OF vt_s this cs_th']
+ − 1695
have "th' = th''" by simp
+ − 1696
with ch' y_ch have "(Th th'', Th th'') \<in> (child s)^+" by auto
+ − 1697
with wf_trancl[OF wf_child[OF vt_s]]
+ − 1698
show False by auto
+ − 1699
next
+ − 1700
fix y
+ − 1701
assume "(Cs cs1, y) \<in> depend s"
+ − 1702
and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"
+ − 1703
with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp
+ − 1704
from unique_depend[OF vt_s this cs_th']
+ − 1705
have "y = Th th''" .
+ − 1706
with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
+ − 1707
from depend_child[OF vt_s this]
+ − 1708
have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
+ − 1709
moreover from ch' y_ch have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
+ − 1710
ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto
+ − 1711
with wf_trancl[OF wf_child[OF vt_s]]
+ − 1712
show False by auto
+ − 1713
qed
+ − 1714
thus "\<exists>cs. (Th th, Cs cs) \<in> depend s' \<and> (Cs cs, Th th'') \<in> depend s'" by auto
+ − 1715
qed
+ − 1716
ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
+ − 1717
by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
+ − 1718
qed
+ − 1719
next
+ − 1720
fix th''
+ − 1721
assume dp': "(Th th', Th th'') \<in> child s"
+ − 1722
show "cp s th'' = cp s' th''"
+ − 1723
apply (subst cp_rec[OF vt_s])
+ − 1724
proof -
+ − 1725
have "preced th'' s = preced th'' s'"
+ − 1726
by (simp add:s_def preced_def)
+ − 1727
moreover {
+ − 1728
fix th1
+ − 1729
assume th1_in: "th1 \<in> children s th''"
+ − 1730
have "cp s th1 = cp s' th1"
+ − 1731
proof(cases "th1 = th'")
+ − 1732
case True
+ − 1733
with eq_cps show ?thesis by simp
+ − 1734
next
+ − 1735
case False
+ − 1736
have neq_th1: "th1 \<noteq> th"
+ − 1737
proof
+ − 1738
assume eq_th1: "th1 = th"
+ − 1739
with dp1 have "(Th th1, Th th') \<in> (depend s)^+"
+ − 1740
by (auto simp:s_dependents_def eq_depend)
+ − 1741
from children_no_dep[OF vt_s _ _ this]
+ − 1742
th1_in dp'
+ − 1743
show False by (auto simp:children_def)
+ − 1744
qed
+ − 1745
show ?thesis
+ − 1746
proof(rule eq_cp)
+ − 1747
show "th \<notin> dependents s th1"
+ − 1748
proof
+ − 1749
assume "th \<in> dependents s th1"
+ − 1750
from dependents_child_unique[OF vt_s _ _ this dp1]
+ − 1751
th1_in dp' have "th1 = th'"
+ − 1752
by (auto simp:children_def)
+ − 1753
with False show False by auto
+ − 1754
qed
+ − 1755
qed
+ − 1756
qed
+ − 1757
}
+ − 1758
ultimately have "{preced th'' s} \<union> (cp s ` children s th'') =
+ − 1759
{preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
+ − 1760
moreover have "children s th'' = children s' th''"
+ − 1761
apply (unfold children_def child_def s_def depend_set_unchanged, simp)
+ − 1762
apply (fold s_def, auto simp:depend_s)
+ − 1763
proof -
+ − 1764
assume "(Cs cs, Th th'') \<in> depend s'"
+ − 1765
with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto
+ − 1766
from dp1 have "(Th th, Th th') \<in> (depend s)^+"
+ − 1767
by (auto simp:s_dependents_def eq_depend)
+ − 1768
from converse_tranclE[OF this]
+ − 1769
obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"
+ − 1770
and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"
+ − 1771
by (auto simp:s_depend_def)
+ − 1772
have eq_cs: "cs1 = cs"
+ − 1773
proof -
+ − 1774
from depend_s have "(Th th, Cs cs) \<in> depend s" by simp
+ − 1775
from unique_depend[OF vt_s this h1]
+ − 1776
show ?thesis by simp
+ − 1777
qed
+ − 1778
have False
+ − 1779
proof(rule converse_tranclE[OF h2])
+ − 1780
assume "(Cs cs1, Th th') \<in> depend s"
+ − 1781
with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp
+ − 1782
from unique_depend[OF vt_s this cs_th']
+ − 1783
have "th' = th''" by simp
+ − 1784
with dp' have "(Th th'', Th th'') \<in> (child s)^+" by auto
+ − 1785
with wf_trancl[OF wf_child[OF vt_s]]
+ − 1786
show False by auto
+ − 1787
next
+ − 1788
fix y
+ − 1789
assume "(Cs cs1, y) \<in> depend s"
+ − 1790
and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"
+ − 1791
with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp
+ − 1792
from unique_depend[OF vt_s this cs_th']
+ − 1793
have "y = Th th''" .
+ − 1794
with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp
+ − 1795
from depend_child[OF vt_s this]
+ − 1796
have "(Th th'', Th th') \<in> (child s)\<^sup>+" .
+ − 1797
moreover from dp' have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto
+ − 1798
ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto
+ − 1799
with wf_trancl[OF wf_child[OF vt_s]]
+ − 1800
show False by auto
+ − 1801
qed
+ − 1802
thus "\<exists>cs. (Th th, Cs cs) \<in> depend s' \<and> (Cs cs, Th th'') \<in> depend s'" by auto
+ − 1803
qed
+ − 1804
ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
+ − 1805
by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
+ − 1806
qed
+ − 1807
qed
+ − 1808
}
+ − 1809
ultimately show ?thesis by auto
+ − 1810
qed
+ − 1811
+ − 1812
end
+ − 1813
+ − 1814
locale step_create_cps =
+ − 1815
fixes s' th prio s
+ − 1816
defines s_def : "s \<equiv> (Create th prio#s')"
+ − 1817
assumes vt_s: "vt step s"
+ − 1818
+ − 1819
context step_create_cps
+ − 1820
begin
+ − 1821
+ − 1822
lemma eq_dep: "depend s = depend s'"
+ − 1823
by (unfold s_def depend_create_unchanged, auto)
+ − 1824
+ − 1825
lemma eq_cp:
+ − 1826
fixes th'
+ − 1827
assumes neq_th: "th' \<noteq> th"
+ − 1828
shows "cp s th' = cp s' th'"
+ − 1829
apply (unfold cp_eq_cpreced cpreced_def)
+ − 1830
proof -
+ − 1831
have nd: "th \<notin> dependents s th'"
+ − 1832
proof
+ − 1833
assume "th \<in> dependents s th'"
+ − 1834
hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+ − 1835
with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
+ − 1836
from converse_tranclE[OF this]
+ − 1837
obtain y where "(Th th, y) \<in> depend s'" by auto
+ − 1838
with dm_depend_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]
+ − 1839
have in_th: "th \<in> threads s'" by auto
+ − 1840
from step_back_step[OF vt_s[unfolded s_def]]
+ − 1841
show False
+ − 1842
proof(cases)
+ − 1843
assume "th \<notin> threads s'"
+ − 1844
with in_th show ?thesis by simp
+ − 1845
qed
+ − 1846
qed
+ − 1847
have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+ − 1848
by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+ − 1849
moreover {
+ − 1850
fix th1
+ − 1851
assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+ − 1852
hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ − 1853
hence "preced th1 s = preced th1 s'"
+ − 1854
proof
+ − 1855
assume "th1 = th'"
+ − 1856
with neq_th
+ − 1857
show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
+ − 1858
next
+ − 1859
assume "th1 \<in> dependents (wq s') th'"
+ − 1860
with nd and eq_dp have "th1 \<noteq> th"
+ − 1861
by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
+ − 1862
thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
+ − 1863
qed
+ − 1864
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1865
((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ − 1866
by (auto simp:image_def)
+ − 1867
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1868
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ − 1869
qed
+ − 1870
+ − 1871
lemma nil_dependents: "dependents s th = {}"
+ − 1872
proof -
+ − 1873
from step_back_step[OF vt_s[unfolded s_def]]
+ − 1874
show ?thesis
+ − 1875
proof(cases)
+ − 1876
assume "th \<notin> threads s'"
+ − 1877
from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this]
+ − 1878
have hdn: " holdents s' th = {}" .
+ − 1879
have "dependents s' th = {}"
+ − 1880
proof -
+ − 1881
{ assume "dependents s' th \<noteq> {}"
+ − 1882
then obtain th' where dp: "(Th th', Th th) \<in> (depend s')^+"
+ − 1883
by (auto simp:s_dependents_def eq_depend)
+ − 1884
from tranclE[OF this] obtain cs' where
+ − 1885
"(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_def)
+ − 1886
with hdn
+ − 1887
have False by (auto simp:holdents_def)
+ − 1888
} thus ?thesis by auto
+ − 1889
qed
+ − 1890
thus ?thesis
+ − 1891
by (unfold s_def s_dependents_def eq_depend depend_create_unchanged, simp)
+ − 1892
qed
+ − 1893
qed
+ − 1894
+ − 1895
lemma eq_cp_th: "cp s th = preced th s"
+ − 1896
apply (unfold cp_eq_cpreced cpreced_def)
+ − 1897
by (insert nil_dependents, unfold s_dependents_def cs_dependents_def, auto)
+ − 1898
+ − 1899
end
+ − 1900
+ − 1901
+ − 1902
locale step_exit_cps =
+ − 1903
fixes s' th prio s
+ − 1904
defines s_def : "s \<equiv> (Exit th#s')"
+ − 1905
assumes vt_s: "vt step s"
+ − 1906
+ − 1907
context step_exit_cps
+ − 1908
begin
+ − 1909
+ − 1910
lemma eq_dep: "depend s = depend s'"
+ − 1911
by (unfold s_def depend_exit_unchanged, auto)
+ − 1912
+ − 1913
lemma eq_cp:
+ − 1914
fixes th'
+ − 1915
assumes neq_th: "th' \<noteq> th"
+ − 1916
shows "cp s th' = cp s' th'"
+ − 1917
apply (unfold cp_eq_cpreced cpreced_def)
+ − 1918
proof -
+ − 1919
have nd: "th \<notin> dependents s th'"
+ − 1920
proof
+ − 1921
assume "th \<in> dependents s th'"
+ − 1922
hence "(Th th, Th th') \<in> (depend s)^+" by (simp add:s_dependents_def eq_depend)
+ − 1923
with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp
+ − 1924
from converse_tranclE[OF this]
+ − 1925
obtain cs' where bk: "(Th th, Cs cs') \<in> depend s'"
+ − 1926
by (auto simp:s_depend_def)
+ − 1927
from step_back_step[OF vt_s[unfolded s_def]]
+ − 1928
show False
+ − 1929
proof(cases)
+ − 1930
assume "th \<in> runing s'"
+ − 1931
with bk show ?thesis
+ − 1932
apply (unfold runing_def readys_def s_waiting_def s_depend_def)
+ − 1933
by (auto simp:cs_waiting_def)
+ − 1934
qed
+ − 1935
qed
+ − 1936
have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
+ − 1937
by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
+ − 1938
moreover {
+ − 1939
fix th1
+ − 1940
assume "th1 \<in> {th'} \<union> dependents (wq s') th'"
+ − 1941
hence "th1 = th' \<or> th1 \<in> dependents (wq s') th'" by auto
+ − 1942
hence "preced th1 s = preced th1 s'"
+ − 1943
proof
+ − 1944
assume "th1 = th'"
+ − 1945
with neq_th
+ − 1946
show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
+ − 1947
next
+ − 1948
assume "th1 \<in> dependents (wq s') th'"
+ − 1949
with nd and eq_dp have "th1 \<noteq> th"
+ − 1950
by (auto simp:eq_depend cs_dependents_def s_dependents_def eq_dep)
+ − 1951
thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)
+ − 1952
qed
+ − 1953
} ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1954
((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))"
+ − 1955
by (auto simp:image_def)
+ − 1956
thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) =
+ − 1957
Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependents (wq s') th'))" by simp
+ − 1958
qed
+ − 1959
+ − 1960
end
+ − 1961
end
+ − 1962