equal
deleted
inserted
replaced
68 To minimize the cost of the recalculation, we derived the following localized alternative |
68 To minimize the cost of the recalculation, we derived the following localized alternative |
69 definition of @{term cp}: |
69 definition of @{term cp}: |
70 *} |
70 *} |
71 |
71 |
72 lemma cp_rec_tG: |
72 lemma cp_rec_tG: |
73 "cp s th = Max (preceds {th} s \<union> cprecs (children (tG s) th) s)" |
73 "cp s th = Max ({preced th s} \<union> cprecs (children (tG s) th) s)" |
74 proof - |
74 proof - |
75 have [simp]: "(cp s \<circ> the_thread \<circ> Th) = cp s" by (rule ext, simp) |
75 have [simp]: "(cp s \<circ> the_thread \<circ> Th) = cp s" by (rule ext, simp) |
76 have [simp]: "(cp s \<circ> the_thread) ` children (tRAG s) (Th th) = |
76 have [simp]: "(cp s \<circ> the_thread) ` children (tRAG s) (Th th) = |
77 cp s ` children (tG s) th" |
77 cp s ` children (tG s) th" |
78 apply (unfold tRAG_def_tG) |
78 apply (unfold tRAG_def_tG) |