equal
deleted
inserted
replaced
787 |
787 |
788 lemma step_depend_p: |
788 lemma step_depend_p: |
789 "vt step (P th cs#s) \<Longrightarrow> |
789 "vt step (P th cs#s) \<Longrightarrow> |
790 depend (P th cs # s) = (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)} |
790 depend (P th cs # s) = (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)} |
791 else depend s \<union> {(Th th, Cs cs)})" |
791 else depend s \<union> {(Th th, Cs cs)})" |
792 apply(unfold s_depend_def wq_def) |
792 apply(simp only: s_depend_def wq_def) |
793 apply (auto split:list.splits prod.splits simp:Let_def cs_waiting_def cs_holding_def) |
793 apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def) |
794 apply(case_tac "csa = cs", auto) |
794 apply(case_tac "csa = cs", auto) |
795 apply(fold wq_def) |
795 apply(fold wq_def) |
796 apply(drule_tac step_back_step) |
796 apply(drule_tac step_back_step) |
797 apply(ind_cases " step s (P (hd (wq s cs)) cs)") |
797 apply(ind_cases " step s (P (hd (wq s cs)) cs)") |
798 apply(auto simp:s_depend_def wq_def cs_holding_def) |
798 apply(auto simp:s_depend_def wq_def cs_holding_def) |