pip: comparison PIPBasics.thy

equal deleted inserted replaced

-:e3cf792db636
+:0f124691c191
 theory PIPBasics
-imports PIPDefs
+imports PIPDefs RTree
 begin
 text {* (* ddd *)
 Following the HOL convention of {\em definitional extension}, we have
 proof -
 from assms[unfolded s_waiting_def, folded wq_def]
 obtain th' where "th' \<in> set (wq s cs)" "th' = hd (wq s cs)"
 by (metis empty_iff hd_in_set list.set(1))
 hence "holding s th' cs"
-by (unfold s_holding_def, fold wq_def, auto)
+unfolding s_holding_def by auto
 from that[OF this] show ?thesis .
 qed
 text {*
 @{term children} in @{term RAG} to the notion of @{term holding}.
 It is a technical lemmas used to prove the two following lemmas.
 *}
 lemma children_RAG_alt_def:
 "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"
-by (unfold s_RAG_def, auto simp:children_def holding_eq)
+by (unfold s_RAG_def, auto simp:children_def s_holding_abv)
 text {*
 The following two lemmas relate @{term holdents} and @{term cntCS}
 to @{term children} in @{term RAG}, so that proofs about
 @{term holdents} and @{term cntCS} can be carried out under
 two nodes are in @{term RAG}.
 *}
 lemma in_RAG_E:
 assumes "(n1, n2) \<in> RAG (s::state)"
 obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
 | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
-using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
+using assms[unfolded s_RAG_def, folded s_waiting_abv s_holding_abv]
 by auto
 text {*
 The following lemmas are the simplification rules
 for @{term count}, @{term cntP}, @{term cntV}.
 apply (simp add: s_RAG_abv s_dependants_def wq_def)
 by (simp add: rtrancl_eq_or_trancl s_RAG_abv s_dependants_def wq_def)
 thus ?thesis by simp
 qed
 thus ?thesis
-by (metis (no_types, lifting) cp_eq cpreced_def eq_dependants
+by (metis (no_types, lifting) cp_eq cpreced_def2 f_image_eq
-f_image_eq the_preced_def)
+s_dependants_abv the_preced_def)
 qed
 text {*
 The following is another definition of @{term cp}.
 *}
 moreover have "th2 = th''"
 proof -
 from h1 have "cs' = cs" by simp
 from assms(2) cs_in[unfolded this]
 have "holding s th'' cs" "holding s th2 cs"
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 from held_unique[OF this]
 show ?thesis by simp
 qed
 ultimately show ?thesis using h(1,2) h1 by auto
 next
 assume otherwise: "th \<in> set (wq s cs)"
 from running_wqE[OF running_th_s this]
 obtain rest where eq_wq: "wq s cs = th#rest" by blast
 with otherwise
 have "holding s th cs"
-by (unfold s_holding_def, fold wq_def, simp)
+unfolding s_holding_def by auto
 hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s"
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 from pip_e[unfolded is_p]
 show False
 proof(cases)
 case (thread_P)
 with cs_th_RAG show ?thesis by auto
 from pip_e[unfolded is_v]
 show ?thesis
 proof(cases)
 case (thread_V)
 from this(2) show ?thesis
-by (unfold rest_def s_holding_def, fold wq_def,
+unfolding s_holding_def
-metis empty_iff list.collapse list.set(1))
+by (metis empty_iff empty_set hd_Cons_tl rest_def)
 qed
 qed
 lemma wq_es_cs:
 "wq (e#s) cs = wq'"
 lemma
 th_not_in_wq: "th \<notin> set (wq s cs)"
 proof -
 from pip_e[unfolded is_exit]
 show ?thesis
-by (cases, unfold holdents_def s_holding_def, fold wq_def,
+apply(cases)
-auto elim!:running_wqE)
+unfolding holdents_def s_holding_def
+by (metis (mono_tags, lifting) empty_iff list.sel(1) mem_Collect_eq running_wqE)
 qed
 lemma wq_threads_kept:
 assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"
 and "th' \<in> set (wq (e#s) cs')"
 and "holding s t c"
 shows "holding (e#s) t c"
 proof -
 from assms(1) have "wq (e#s) c = wq s c"  by auto
 from assms(2)[unfolded s_holding_def, folded wq_def,
-folded this, unfolded wq_def, folded s_holding_def]
+folded this, folded s_holding_def]
 show ?thesis .
 qed
 lemma holding_esI1:
 assumes "holding s t c"
 using next_th_taker taker_def waiting_set_eq
 by fastforce
 lemma holding_taker:
 shows "holding (e#s) taker cs"
-by (unfold s_holding_def, fold wq_def, unfold wq_es_cs,
+by (unfold s_holding_def, unfold wq_es_cs,
 auto simp:neq_wq' taker_def)
 lemma waiting_esI2:
 assumes "waiting s t cs"
 and "t \<noteq> taker"
 from that(1)[OF True this] show ?thesis .
 next
 case False
 hence "wq (e#s) c = wq s c" by auto
 from assms[unfolded s_holding_def, folded wq_def,
-unfolded this, unfolded wq_def, folded s_holding_def]
+unfolded this, folded s_holding_def]
 have "holding s t c"  .
 from that(2)[OF False this] show ?thesis .
 qed
 end
 show ?thesis by auto
 next
 case False
 hence "wq (e#s) c = wq s c" by auto
 from assms[unfolded s_holding_def, folded wq_def,
-unfolded this, unfolded wq_def, folded s_holding_def]
+unfolded this, folded s_holding_def]
 have "holding s t c"  .
 from that[OF False this] show ?thesis .
 qed
 end
 proof(cases rule:h_n.waiting_esE)
 case 1
 with waiting(1,2)
 show ?thesis
 by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
-fold waiting_eq, auto)
+fold s_waiting_abv, auto)
 next
 case 2
 with waiting(1,2)
 show ?thesis
 by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
-fold waiting_eq, auto)
+fold s_waiting_abv, auto)
 qed
 next
 case True
 interpret h_e: valid_trace_v_e s e th cs
 by (unfold_locales, insert True, simp)
 proof(cases rule:h_e.waiting_esE)
 case 1
 with waiting(1,2)
 show ?thesis
 by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def,
-fold waiting_eq, auto)
+fold s_waiting_abv, auto)
 qed
 qed
 next
 case (holding th' cs')
 show ?thesis
 proof(cases rule:h_n.holding_esE)
 case 1
 with holding(1,2)
 show ?thesis
 by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
-fold waiting_eq, auto)
+fold s_waiting_abv, auto)
 next
 case 2
 with holding(1,2)
 show ?thesis
 by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
-fold holding_eq, auto)
+fold s_holding_abv, auto)
 qed
 next
 case True
 interpret h_e: valid_trace_v_e s e th cs
 by (unfold_locales, insert True, simp)
 proof(cases rule:h_e.holding_esE)
 case 1
 with holding(1,2)
 show ?thesis
 by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def,
-fold holding_eq, auto)
+fold s_holding_abv, auto)
 qed
 qed
 qed
 next
 fix n1 n2
 thus ?thesis
 proof
 assume "n2 = Th h_n.taker \<and> n1 = Cs cs"
 with h_n.holding_taker
 show ?thesis
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 next
 assume h: "(n1, n2) \<in> RAG s \<and>
 (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)"
 hence "(n1, n2) \<in> RAG s" by simp
 thus ?thesis
 from h_n.waiting_esI2[OF waiting(3)[unfolded True] neq_th', folded True]
 show ?thesis .
 qed
 qed
 thus ?thesis using waiting(1,2)
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 next
 case (holding th' cs')
 from h this(1,2)
 have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto
 hence "holding (e#s) th' cs'"
 assume "th' \<noteq> th"
 from holding_esI1[OF holding(3) this]
 show ?thesis .
 qed
 thus ?thesis using holding(1,2)
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 qed
 qed
 next
 case True
 interpret h_e: valid_trace_v_e s e th cs
 show ?thesis
 proof(cases rule:in_RAG_E)
 case (waiting th' cs')
 from h_e.waiting_esI2[OF this(3)]
 show ?thesis using waiting(1,2)
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 next
 case (holding th' cs')
 with h_s(2)
 have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto
 thus ?thesis
 proof
 assume neq_cs: "cs' \<noteq> cs"
 from holding_esI2[OF this holding(3)]
 show ?thesis using holding(1,2)
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 next
 assume "th' \<noteq> th"
 from holding_esI1[OF holding(3) this]
 show ?thesis using holding(1,2)
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 qed
 qed
 qed
 qed
 assumes "holding s th' cs'"
 shows "holding (e#s) th' cs'"
 proof(cases "cs' = cs")
 case False
 hence "wq (e#s) cs' = wq s cs'" by simp
-with assms show ?thesis unfolding holding_raw_def holding_eq by auto
+with assms show ?thesis unfolding holding_raw_def s_holding_abv by auto
 next
 case True
 from assms[unfolded s_holding_def, folded wq_def]
 obtain rest where eq_wq: "wq s cs' = th'#rest"
 by (metis empty_iff list.collapse list.set(1))
 hence "wq (e#s) cs' = th'#(rest@[th])"
 by (simp add: True wq_es_cs)
 thus ?thesis
-by (simp add: holding_raw_def holding_eq)
+by (simp add: holding_raw_def s_holding_abv)
 qed
 end
 lemma (in valid_trace_p) th_not_waiting: "\<not> waiting s th c"
 proof -
 lemma holding_es_th_cs:
 shows "holding (e#s) th cs"
 proof -
 from wq_es_cs'
 have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto
-thus ?thesis unfolding holding_raw_def holding_eq by blast
+thus ?thesis unfolding holding_raw_def s_holding_abv by blast
 qed
 lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)"
-by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto)
+by (unfold s_RAG_def, fold s_holding_abv, insert holding_es_th_cs, auto)
 lemma waiting_esE:
 assumes "waiting (e#s) th' cs'"
 obtains "waiting s th' cs'"
 using assms
 have "th' = th" by simp
 from that(2)[OF True this] show ?thesis .
 next
 case False
 have "holding s th' cs'" using assms
-using False unfolding holding_raw_def holding_eq by auto
+using False unfolding holding_raw_def s_holding_abv by auto
 from that(1)[OF False this] show ?thesis .
 qed
 lemma RAG_es: "RAG (e # s) =  RAG s \<union> {(Cs cs, Th th)}" (is "?L = ?R")
 proof(rule rel_eqI)
 from this(3)
 show ?thesis
 proof(cases rule:waiting_esE)
 case 1
 thus ?thesis using waiting(1,2)
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 qed
 next
 case (holding th' cs')
 from this(3)
 show ?thesis
 proof(cases rule:holding_esE)
 case 1
 with holding(1,2)
-show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
+show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto)
 next
 case 2
 with holding(1,2) show ?thesis by auto
 qed
 qed
 thus ?thesis
 proof(cases rule:in_RAG_E)
 case (waiting th' cs')
 from waiting_kept[OF this(3)]
 show ?thesis using waiting(1,2)
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 next
 case (holding th' cs')
 from holding_kept[OF this(3)]
 show ?thesis using holding(1,2)
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 qed
 next
 assume "n1 = Cs cs \<and> n2 = Th th"
 with holding_es_th_cs
 show ?thesis
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 qed
 qed
 end
 lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]"
 by (simp add: wq_es_cs wq_s_cs)
 lemma waiting_es_th_cs: "waiting (e#s) th cs"
-using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs
+using th_not_in_wq s_waiting_abv wq_es_cs' wq_s_cs
-by (simp add: s_waiting_def wq_def wq_es_cs)
+using Un_iff list.sel(1) list.set_intros(1) s_waiting_def
+set_append wq_def wq_es_cs by auto
 lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"
-by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, insert waiting_es_th_cs, auto)
 lemma holding_esE:
 assumes "holding (e#s) th' cs'"
 obtains "holding s th' cs'"
 using assms
 from this(3)
 show ?thesis
 proof(cases rule:waiting_esE)
 case 1
 thus ?thesis using waiting(1,2)
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 next
 case 2
 thus ?thesis using waiting(1,2) by auto
 qed
 next
 from this(3)
 show ?thesis
 proof(cases rule:holding_esE)
 case 1
 with holding(1,2)
-show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
+show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto)
 qed
 qed
 next
 fix n1 n2
 assume "(n1, n2) \<in> ?R"
 thus ?thesis
 proof(cases rule:in_RAG_E)
 case (waiting th' cs')
 from waiting_kept[OF this(3)]
 show ?thesis using waiting(1,2)
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 next
 case (holding th' cs')
 from holding_kept[OF this(3)]
 show ?thesis using holding(1,2)
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 qed
 next
 assume "n1 = Th th \<and> n2 = Cs cs"
 thus ?thesis using RAG_edge by auto
 qed
 from tranclD[OF this]
 obtain cs' where h: "(Th taker, Cs cs') \<in> ?A"
 "(Th taker, Cs cs') \<in> RAG s"
 by (unfold s_RAG_def, auto)
 from this(2) have "waiting s taker cs'"
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 from waiting_unique[OF this waiting_taker]
 have "cs' = cs" .
 from h(1)[unfolded this] show False by auto
 qed
 ultimately show ?thesis by auto
 by (unfold rtrancl_eq_or_trancl, auto)
 from tranclD[OF this]
 obtain cs' where h: "(Th th, Cs cs') \<in> RAG s"
 by (unfold s_RAG_def, auto)
 hence "waiting s th cs'"
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 with th_not_waiting show False by auto
 qed
 ultimately show ?thesis by auto
 qed
 thus ?thesis by (unfold RAG_es, simp)
 context valid_trace
 begin
 lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
-apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
+apply(unfold s_RAG_def, auto, fold s_waiting_abv s_holding_abv)
 by(auto elim:waiting_unique held_unique)
 lemma sgv_RAG: "single_valued (RAG s)"
 using unique_RAG by (auto simp:single_valued_def)
 have "(node, b) \<in> ((RAG s)\<^sup>+)" by auto
 from tranclE[OF this]
 obtain n where "(n, b) \<in> RAG s" by auto
 from this[unfolded Cs]
 obtain th1 where "waiting s th1 cs"
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 from waiting_holding[OF this]
 obtain th2 where "holding s th2 cs" .
 hence "(Cs cs, Th th2) \<in> RAG s"
-by (unfold s_RAG_def, fold holding_eq, auto)
+by (unfold s_RAG_def, fold s_holding_abv, auto)
 with h_b(2)[unfolded Cs, rule_format]
 have False by auto
 thus ?thesis by auto
 qed auto
 have "th' \<in> readys s"
 proof -
 from h_b(2)[unfolded eq_b]
 have "\<forall>cs. \<not> waiting s th' cs"
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 moreover have "th' \<in> threads s"
 proof(rule rg_RAG_threads)
 from tranclD[OF h_b(1), unfolded eq_b]
 obtain z where "(z, Th th') \<in> (RAG s)" by auto
 thus "Th th' \<in> Range (RAG s)" by auto
 assume otherwise: "xs' \<noteq> []"
 from rpath_plus[OF less_1(3) this]
 have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" .
 from tranclD[OF this]
 obtain cs where "waiting s th1 cs"
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 with running_1 show False
 by (unfold running_def readys_def, auto)
 qed
 ultimately have "xs2 = xs1" by simp
 from rpath_dest_eq[OF rp1 rp2[unfolded this]]
 assume otherwise: "xs' \<noteq> []"
 from rpath_plus[OF less_2(3) this]
 have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" .
 from tranclD[OF this]
 obtain cs where "waiting s th2 cs"
-by (unfold s_RAG_def, fold waiting_eq, auto)
+by (unfold s_RAG_def, fold s_waiting_abv, auto)
 with running_2 show False
 by (unfold running_def readys_def, auto)
 qed
 ultimately have "xs2 = xs1" by simp
 from rpath_dest_eq[OF rp1 rp2[unfolded this]]
 hence "(Th th1, Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)
 from tranclD[OF this]
 obtain z where "(Th th1, z) \<in> RAG s" by auto
 from this[unfolded s_RAG_def, folded wq_def]
 obtain cs' where "waiting s th1 cs'"
-by (auto simp:waiting_eq)
+by (auto simp:s_waiting_abv)
 with assms(1) show False by (auto simp:readys_def)
 qed
 next
 case (less_2 xs3)
 from rpath_star[OF this(3)]
 hence "(Th th2, Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)
 from tranclD[OF this]
 obtain z where "(Th th2, z) \<in> RAG s" by auto
 from this[unfolded s_RAG_def, folded wq_def]
 obtain cs' where "waiting s th2 cs'"
-by (auto simp:waiting_eq)
+by (auto simp:s_waiting_abv)
 with assms(2) show False by (auto simp:readys_def)
 qed
 qed
 } thus ?thesis by auto
 qed
 context valid_trace_p_w
 begin
 lemma holding_s_holder: "holding s holder cs"
-by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
+by (unfold s_holding_def, unfold wq_s_cs, auto)
 lemma holding_es_holder: "holding (e#s) holder cs"
-by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto)
+by (unfold s_holding_def, unfold wq_es_cs wq_s_cs, auto)
 lemma holdents_es:
 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
 proof -
 { fix cs'
 next
 case False
 hence "wq (e#s) cs' = wq s cs'" by simp
 from h[unfolded s_holding_def, folded wq_def, unfolded this]
 show ?thesis
-by (unfold s_holding_def, fold wq_def, auto)
+by (unfold s_holding_def, auto)
 qed
 hence "cs' \<in> ?R" by (auto simp:holdents_def)
 } moreover {
 fix cs'
 assume "cs' \<in> ?R"
 next
 case False
 hence "wq s cs' = wq (e#s) cs'" by simp
 from h[unfolded s_holding_def, folded wq_def, unfolded this]
 show ?thesis
-by (unfold s_holding_def, fold wq_def, auto)
+by (unfold s_holding_def, auto)
 qed
 hence "cs' \<in> ?L" by (auto simp:holdents_def)
 } ultimately show ?thesis by auto
 qed
 with assms show False by simp
 qed
 from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]]
 have "th' \<in> set (wq s cs') \<and> th' = hd (wq s cs')" .
 hence "cs' \<in> ?R"
-by (unfold holdents_def s_holding_def, fold wq_def, auto)
+by (unfold holdents_def s_holding_def, auto)
 } moreover {
 fix cs'
 assume "cs' \<in> ?R"
 hence "holding s th' cs'" by (auto simp:holdents_def)
 from holding_kept[OF this]
 context valid_trace_v
 begin
 lemma holding_th_cs_s:
 "holding s th cs"
-by  (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
+by  (unfold s_holding_def, unfold wq_s_cs, auto)
 lemma th_ready_s [simp]: "th \<in> readys s"
 using running_th_s
 by (unfold running_def readys_def, auto)
 case False
 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
 from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
 show ?thesis
-by (unfold holdents_def s_holding_def, fold wq_def, auto)
+by (unfold holdents_def s_holding_def, auto)
 next
 case True
 from h[unfolded this]
 have "holding (e#s) th' cs" by (auto simp:holdents_def)
 from held_unique[OF this holding_taker]
 case False
 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
 from h have "holding s th' cs'" by (auto simp:holdents_def)
 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
 show ?thesis
-by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
+by (unfold holdents_def s_holding_def, insert eq_wq, simp)
 next
 case True
 from h[unfolded this]
 have "holding s th' cs" by (auto simp:holdents_def)
 from held_unique[OF this holding_th_cs_s]
 case False
 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
 from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
 show ?thesis
-by (unfold holdents_def s_holding_def, fold wq_def, auto)
+by (unfold holdents_def s_holding_def, auto)
 next
 case True
 from h[unfolded this]
 have "holding (e#s) th' cs" by (auto simp:holdents_def)
 from this[unfolded s_holding_def, folded wq_def,
 case False
 hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
 from h have "holding s th' cs'" by (auto simp:holdents_def)
 from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
 show ?thesis
-by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
+by (unfold holdents_def s_holding_def, insert eq_wq, simp)
 next
 case True
 from h[unfolded this]
 have "holding s th' cs" by (auto simp:holdents_def)
 from held_unique[OF this holding_th_cs_s]
 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
 proof -
 { fix cs'
 assume h: "cs' \<in> ?L"
 hence "cs' \<in> ?R"
-by (unfold holdents_def s_holding_def, fold wq_def,
+by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
-unfold wq_kept, auto)
 } moreover {
 fix cs'
 assume h: "cs' \<in> ?R"
 hence "cs' \<in> ?L"
-by (unfold holdents_def s_holding_def, fold wq_def,
+by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
-unfold wq_kept, auto)
 } ultimately show ?thesis by auto
 qed
 lemma cntCS_kept [simp]:
 assumes "th' \<noteq> th"
 lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"
 proof
 assume "holding (e # s) th cs'"
 from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
 have "holding s th cs'"
-by (unfold s_holding_def, fold wq_def, auto)
+by (unfold s_holding_def, auto)
 with not_holding_th_s
 show False by simp
 qed
 lemma ready_th_es [simp]: "th \<notin> readys (e#s)"
 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
 proof -
 { fix cs'
 assume h: "cs' \<in> ?L"
 hence "cs' \<in> ?R"
-by (unfold holdents_def s_holding_def, fold wq_def,
+by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
-unfold wq_kept, auto)
 } moreover {
 fix cs'
 assume h: "cs' \<in> ?R"
 hence "cs' \<in> ?L"
-by (unfold holdents_def s_holding_def, fold wq_def,
+by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
-unfold wq_kept, auto)
 } ultimately show ?thesis by auto
 qed
 lemma cntCS_kept [simp]:
 assumes "th' \<noteq> th"
 shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
 proof -
 { fix cs'
 assume h: "cs' \<in> ?L"
 hence "cs' \<in> ?R"
-by (unfold holdents_def s_holding_def, fold wq_def,
+by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
-unfold wq_kept, auto)
 } moreover {
 fix cs'
 assume h: "cs' \<in> ?R"
 hence "cs' \<in> ?L"
-by (unfold holdents_def s_holding_def, fold wq_def,
+by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
-unfold wq_kept, auto)
 } ultimately show ?thesis by auto
 qed
 lemma cntCS_kept [simp]:
 shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")
 lemma cnp_cnv_cncs: "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
 proof(induct rule:ind)
 case Nil
 thus ?case
-by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def
+unfolding cntP_def  cntV_def pvD_def cntCS_def holdents_def s_holding_def
-s_holding_def, simp)
+by(simp add: wq_def)
 next
 case (Cons s e)
 interpret vt_e: valid_trace_e s e using Cons by simp
 show ?case
 proof(cases e)
 qed
 lemma count_eq_tRAG_plus:
 assumes "cntP s th = cntV s th"
 shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
-using assms eq_pv_dependants dependants_alt_def eq_dependants by auto
+using assms count_eq_RAG_plus dependants_alt_def s_dependants_def by blast
 lemma count_eq_tRAG_plus_Th:
 assumes "cntP s th = cntV s th"
 shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
 using count_eq_tRAG_plus[OF assms] by auto
 proof(cases "th \<in> threads s")
 case True
 with dtc
 have "th \<in> readys s"
 by (unfold readys_def detached_def Field_def Domain_def Range_def,
-auto simp:waiting_eq s_RAG_def)
+auto simp:s_waiting_abv s_RAG_def)
 with cncs_z  show ?thesis using cnp_cnv_cncs by (simp add:pvD_def)
 next
 case False
 with cncs_z and cnp_cnv_cncs show ?thesis by (simp add:pvD_def)
 qed

changeset 130	0f124691c191
parent 129	e3cf792db636
child 131	6a7a8c51d42f