154 The following four lemmas relate the @{term wq} |
154 The following four lemmas relate the @{term wq} |
155 and non-@{term wq} versions of @{term waiting}, @{term holding}, |
155 and non-@{term wq} versions of @{term waiting}, @{term holding}, |
156 @{term dependants} and @{term cp}. |
156 @{term dependants} and @{term cp}. |
157 *} |
157 *} |
158 |
158 |
159 lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs" |
159 lemma waiting_eq: "waiting s th cs = waiting_raw (wq s) th cs" |
160 by (unfold s_waiting_def cs_waiting_def wq_def, auto) |
160 by (unfold s_waiting_def cs_waiting_raw wq_def, auto) |
161 |
161 |
162 lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs" |
162 lemma holding_eq: "holding (s::state) th cs = holding_raw (wq s) th cs" |
163 by (unfold s_holding_def wq_def cs_holding_def, simp) |
163 by (unfold s_holding_def wq_def cs_holding_raw, simp) |
164 |
164 |
165 lemma eq_dependants: "dependants (wq s) = dependants s" |
165 lemma eq_dependants: "dependants_raw (wq s) = dependants s" |
166 by (simp add: s_dependants_abv wq_def) |
166 by (simp add: s_dependants_abv wq_def) |
167 |
167 |
168 lemma cp_eq: "cp s th = cpreced (wq s) s th" |
168 lemma cp_eq: "cp s th = cpreced (wq s) s th" |
169 unfolding cp_def wq_def |
169 unfolding cp_def wq_def |
170 apply(induct s rule: schs.induct) |
170 apply(induct s rule: schs.induct) |
390 by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", |
390 by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", |
391 insert assms V, auto simp:cntV_def) |
391 insert assms V, auto simp:cntV_def) |
392 qed (insert assms, auto simp:cntV_def) |
392 qed (insert assms, auto simp:cntV_def) |
393 |
393 |
394 lemma eq_RAG: |
394 lemma eq_RAG: |
395 "RAG (wq s) = RAG s" |
395 "RAG_raw (wq s) = RAG s" |
396 by (unfold cs_RAG_def s_RAG_def, auto) |
396 by (unfold cs_RAG_raw s_RAG_def, auto) |
397 |
397 |
398 text {* |
398 text {* |
399 The following three lemmas shows the shape |
399 The following three lemmas shows the shape |
400 of nodes in @{term tRAG}. |
400 of nodes in @{term tRAG}. |
401 *} |
401 *} |
592 *} |
592 *} |
593 lemma cp_alt_def: |
593 lemma cp_alt_def: |
594 "cp s th = |
594 "cp s th = |
595 Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})" |
595 Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})" |
596 proof - |
596 proof - |
597 have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) = |
597 have "Max (the_preced s ` ({th} \<union> dependants_raw (wq s) th)) = |
598 Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
598 Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" |
599 (is "Max (_ ` ?L) = Max (_ ` ?R)") |
599 (is "Max (_ ` ?L) = Max (_ ` ?R)") |
600 proof - |
600 proof - |
601 have "?L = ?R" |
601 have "?L = ?R" |
602 by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def) |
602 by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_raw s_RAG_def subtree_def) |
603 thus ?thesis by simp |
603 thus ?thesis by simp |
604 qed |
604 qed |
605 thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp) |
605 thus ?thesis by (unfold cp_eq cpreced_def, fold the_preced_def, simp) |
606 qed |
606 qed |
607 |
607 |