equal
deleted
inserted
replaced
79 have "Max (the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#s)) (Th th')}) = |
79 have "Max (the_preced (e#s) ` {th'a. Th th'a \<in> subtree (RAG (e#s)) (Th th')}) = |
80 Max (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')})" |
80 Max (the_preced s ` {th'a. Th th'a \<in> subtree (RAG s) (Th th')})" |
81 (is "Max (?f ` ?S1) = Max (?g ` ?S2)") |
81 (is "Max (?f ` ?S1) = Max (?g ` ?S2)") |
82 proof - |
82 proof - |
83 -- {* The base sets are equal. *} |
83 -- {* The base sets are equal. *} |
84 have "?S1 = ?S2" using RAG_unchanged by simp |
84 have "?S1 = ?S2" using RAG_es by simp |
85 -- {* The function values on the base set are equal as well. *} |
85 -- {* The function values on the base set are equal as well. *} |
86 moreover have "\<forall> e \<in> ?S2. ?f e = ?g e" |
86 moreover have "\<forall> e \<in> ?S2. ?f e = ?g e" |
87 proof |
87 proof |
88 fix th1 |
88 fix th1 |
89 assume "th1 \<in> ?S2" |
89 assume "th1 \<in> ?S2" |
160 text {* |
160 text {* |
161 The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, |
161 The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, |
162 which represents the case when there is another thread @{text "th'"} |
162 which represents the case when there is another thread @{text "th'"} |
163 to take over the critical resource released by the initiating thread @{text "th"}. |
163 to take over the critical resource released by the initiating thread @{text "th"}. |
164 *} |
164 *} |
|
165 |
|
166 lemma (in valid_trace_v) |
|
167 the_preced_es: "the_preced (e#s) = the_preced s" |
|
168 proof |
|
169 fix th' |
|
170 show "the_preced (e # s) th' = the_preced s th'" |
|
171 by (unfold the_preced_def preced_def is_v, simp) |
|
172 qed |
165 |
173 |
166 context valid_trace_v_n |
174 context valid_trace_v_n |
167 begin |
175 begin |
168 |
176 |
169 lemma sub_RAGs': |
177 lemma sub_RAGs': |
373 using holding_s_holder |
381 using holding_s_holder |
374 by (unfold s_RAG_def, fold holding_eq, auto) |
382 by (unfold s_RAG_def, fold holding_eq, auto) |
375 |
383 |
376 lemma tRAG_s: |
384 lemma tRAG_s: |
377 "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}" |
385 "tRAG (e#s) = tRAG s \<union> {(Th th, Th holder)}" |
378 using local.RAG_tRAG_transfer[OF RAG_es cs_held] . |
386 using RAG_tRAG_transfer[OF RAG_es cs_held] . |
379 |
387 |
380 lemma cp_kept: |
388 lemma cp_kept: |
381 assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)" |
389 assumes "Th th'' \<notin> ancestors (tRAG (e#s)) (Th th)" |
382 shows "cp (e#s) th'' = cp s th''" |
390 shows "cp (e#s) th'' = cp s th''" |
383 proof - |
391 proof - |
559 |
567 |
560 context valid_trace_create |
568 context valid_trace_create |
561 begin |
569 begin |
562 |
570 |
563 lemma tRAG_kept: "tRAG (e#s) = tRAG s" |
571 lemma tRAG_kept: "tRAG (e#s) = tRAG s" |
564 by (unfold tRAG_alt_def RAG_unchanged, auto) |
572 by (unfold tRAG_alt_def RAG_es, auto) |
565 |
573 |
566 lemma preced_kept: |
574 lemma preced_kept: |
567 assumes "th' \<noteq> th" |
575 assumes "th' \<noteq> th" |
568 shows "the_preced (e#s) th' = the_preced s th'" |
576 shows "the_preced (e#s) th' = the_preced s th'" |
569 by (unfold the_preced_def preced_def is_create, insert assms, auto) |
577 by (unfold the_preced_def preced_def is_create, insert assms, auto) |
632 shows "the_preced (e#s) th' = the_preced s th'" |
640 shows "the_preced (e#s) th' = the_preced s th'" |
633 using assms |
641 using assms |
634 by (unfold the_preced_def is_exit preced_def, simp) |
642 by (unfold the_preced_def is_exit preced_def, simp) |
635 |
643 |
636 lemma tRAG_kept: "tRAG (e#s) = tRAG s" |
644 lemma tRAG_kept: "tRAG (e#s) = tRAG s" |
637 by (unfold tRAG_alt_def RAG_unchanged, auto) |
645 by (unfold tRAG_alt_def RAG_es, auto) |
638 |
646 |
639 lemma th_RAG: "Th th \<notin> Field (RAG s)" |
647 lemma th_RAG: "Th th \<notin> Field (RAG s)" |
640 proof - |
648 proof - |
641 have "Th th \<notin> Range (RAG s)" |
649 have "Th th \<notin> Range (RAG s)" |
642 proof |
650 proof |