equal
deleted
inserted
replaced
2774 qed |
2774 qed |
2775 |
2775 |
2776 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool" |
2776 definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool" |
2777 where "detached s th \<equiv> (Th th \<notin> Field (depend s))" |
2777 where "detached s th \<equiv> (Th th \<notin> Field (depend s))" |
2778 |
2778 |
|
2779 thm Field_def |
|
2780 |
2779 lemma detached_intro: |
2781 lemma detached_intro: |
2780 fixes s th |
2782 fixes s th |
2781 assumes vt: "vt s" |
2783 assumes vt: "vt s" |
2782 and eq_pv: "cntP s th = cntV s th" |
2784 and eq_pv: "cntP s th = cntV s th" |
2783 shows "detached s th" |
2785 shows "detached s th" |
2801 proof - |
2803 proof - |
2802 from card_0_eq [OF finite_holding [OF vt]] and cncs_zero |
2804 from card_0_eq [OF finite_holding [OF vt]] and cncs_zero |
2803 have "holdents s th = {}" |
2805 have "holdents s th = {}" |
2804 by (simp add:cntCS_def) |
2806 by (simp add:cntCS_def) |
2805 thus ?thesis |
2807 thus ?thesis |
2806 by (auto simp:holdents_def, case_tac x, |
2808 apply(auto simp:holdents_def) |
2807 auto simp:holdents_def s_depend_def) |
2809 apply(case_tac a) |
|
2810 apply(auto simp:holdents_def s_depend_def) |
|
2811 done |
2808 qed |
2812 qed |
2809 ultimately show ?thesis |
2813 ultimately show ?thesis |
2810 apply (auto simp:detached_def Field_def Domain_def readys_def) |
2814 apply (auto simp:detached_def Field_def Domain_def readys_def) |
2811 apply (case_tac y, auto simp:s_depend_def) |
2815 apply (case_tac b, auto simp:s_depend_def) |
2812 by (erule_tac x = "nat" in allE, simp add: eq_waiting) |
2816 by (erule_tac x = "nat" in allE, simp add: eq_waiting) |
2813 qed |
2817 qed |
2814 qed |
2818 qed |
2815 |
2819 |
2816 lemma detached_elim: |
2820 lemma detached_elim: |