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