equal
deleted
inserted
replaced
243 assume "{} \<noteq> {}" show ?case by auto |
243 assume "{} \<noteq> {}" show ?case by auto |
244 qed |
244 qed |
245 qed |
245 qed |
246 |
246 |
247 definition child :: "state \<Rightarrow> (node \<times> node) set" |
247 definition child :: "state \<Rightarrow> (node \<times> node) set" |
248 where "child s = |
248 where "child s \<equiv> |
249 {(Th th', Th th) | th th'. \<exists> cs. (Th th', Cs cs) \<in> depend s \<and> (Cs cs, Th th) \<in> depend 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 |
250 |
251 definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set" |
251 definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set" |
252 where "children s th = {th'. (Th th', Th th) \<in> child s}" |
252 where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}" |
253 |
253 |
|
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 |
254 |
257 |
255 lemma children_dependents: "children s th \<subseteq> dependents (wq s) th" |
258 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) |
259 by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend) |
257 |
260 |
258 lemma child_unique: |
261 lemma child_unique: |
1002 |
1005 |
1003 context step_v_cps_nt |
1006 context step_v_cps_nt |
1004 begin |
1007 begin |
1005 |
1008 |
1006 lemma depend_s: |
1009 lemma depend_s: |
1007 "depend s = (depend s' - {(Cs cs, Th th)} - {(Th th', Cs cs)}) \<union> |
1010 "depend s = (depend s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union> |
1008 {(Cs cs, Th th')}" |
1011 {(Cs cs, Th th')}" |
1009 proof - |
1012 proof - |
1010 from step_depend_v[OF vt_s[unfolded s_def], folded s_def] |
1013 from step_depend_v[OF vt_s[unfolded s_def], folded s_def] |
1011 and nt show ?thesis by (auto intro:next_th_unique) |
1014 and nt show ?thesis by (auto intro:next_th_unique) |
1012 qed |
1015 qed |