pip: comparison PIPBasics.thy

equal deleted inserted replaced

-:a88af0e4731f
+:38c6acf03f68
 theory PIPBasics
 imports PIPDefs
 begin
 text {* (* ddd *)
 Following the HOL convention of {\em definitional extension}, we have
-given a concise and miniature model of PIP. To assure ourselves of
+given a concise and miniature model of PIP. To assure ourselves of the
-the correctness of this model, we are going to derive a series of
+correctness of this model, we are going to derive a series of expected
-expected properties out of it.
+properties out of it.
 This file contains the very basic properties, useful for self-assurance,
-as well as for deriving more advance properties concerning
+as well as for deriving more advance properties concerning the correctness
-the correctness and implementation of PIP.
+and implementation of PIP. *}
-*}
 section {* Generic auxiliary lemmas *}
 lemma rel_eqI:
 text {* The following lemma is used in Correctness.thy *}
 lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
 by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)
 text {*
-The follow lemma says if a resource is waited for, it must be held
-by someone else.
+The following lemma says that if a resource is waited for, it must be held
-*}
+by someone else. *}
 lemma waiting_holding:
 assumes "waiting (s::state) th cs"
 obtains th' where "holding s th' cs"
 proof -
 from assms[unfolded s_waiting_def, folded wq_def]
 hence "holding s th' cs"
 by (unfold s_holding_def, fold wq_def, auto)
 from that[OF this] show ?thesis .
 qed
-text {*
-The following four lemmas relate the @{term wq}
-and non-@{term wq} versions of @{term waiting}, @{term holding},
-@{term dependants} and @{term cp}.
-*}
-lemma waiting_eq: "waiting s th cs = waiting_raw (wq s) th cs"
-by  (unfold s_waiting_def cs_waiting_raw wq_def, auto)
-lemma holding_eq: "holding (s::state) th cs = holding_raw (wq s) th cs"
-by (unfold s_holding_def wq_def cs_holding_raw, simp)
-lemma eq_dependants: "dependants_raw (wq s) = dependants s"
-by (simp add: s_dependants_abv wq_def)
-lemma cp_eq: "cp s th = cpreced (wq s) s th"
-unfolding cp_def wq_def
-apply(induct s rule: schs.induct)
-apply(simp add: Let_def cpreced_initial)
-apply(simp add: Let_def)
-apply(simp add: Let_def)
-apply(simp add: Let_def)
-apply(subst (2) schs.simps)
-apply(simp add: Let_def)
-apply(subst (2) schs.simps)
-apply(simp add: Let_def)
-done
 text {*
 The following @{text "children_RAG_alt_def"} relates
 @{term children} in @{term RAG} to the notion of @{term holding}.
 It is a technical lemmas used to prove the two following lemmas.
 apply (unfold children_RAG_alt_def cntCS_def holdents_def)
 by (rule card_image[symmetric], auto simp:inj_on_def)
 text {*
 The following two lemmas show the inclusion relations
-among three key sets, namely @{term runing}, @{term readys}
+among three key sets, namely @{term running}, @{term readys}
 and @{term threads}.
 *}
-lemma runing_ready:
+lemma running_ready:
-shows "runing s \<subseteq> readys s"
+shows "running s \<subseteq> readys s"
-unfolding runing_def readys_def
+unfolding running_def readys_def
 by auto
 lemma readys_threads:
 shows "readys s \<subseteq> threads s"
 unfolding readys_def
 The following lemma says that if a thread is running,
 it must be the head of every waiting queue it is in.
 In other words, a running thread must have got every
 resource it has requested.
 *}
-lemma runing_wqE:
+lemma running_wqE:
-assumes "th \<in> runing s"
+assumes "th \<in> running s"
 and "th \<in> set (wq s cs)"
 obtains rest where "wq s cs = th#rest"
 proof -
 from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest"
 by (metis empty_iff list.exhaust list.set(1))
 hence "th \<noteq> hd (wq s cs)" using eq_wq by auto
 with assms(2)
 have "waiting s th cs"
 by (unfold s_waiting_def, fold wq_def, auto)
 with assms show False
-by (unfold runing_def readys_def, auto)
+by (unfold running_def readys_def, auto)
 qed
 with eq_wq that show ?thesis by metis
 qed
 text {*
 show ?thesis using that
 by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)",
 insert assms V, auto simp:cntV_def)
 qed (insert assms, auto simp:cntV_def)
-lemma eq_RAG:
-"RAG_raw (wq s) = RAG s"
-by (unfold cs_RAG_raw s_RAG_def, auto)
 text {*
 The following three lemmas shows the shape
 of nodes in @{term tRAG}.
 *}
 is handy to use once the abstract theory of {\em relational graph}
 (and specifically {\em relational tree} and {\em relational forest})
 are in place.
 *}
 lemma cp_alt_def:
-"cp s th =
+"cp s th =  Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
-Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
+proof -
-proof -
+have "Max (the_preced s ` ({th} \<union> dependants s th)) =
-have "Max (the_preced s ` ({th} \<union> dependants_raw (wq s) th)) =
 Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
 (is "Max (_ ` ?L) = Max (_ ` ?R)")
 proof -
 have "?L = ?R"
-by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_raw s_RAG_def subtree_def)
+unfolding subtree_def
+apply(auto)
+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 (unfold cp_eq cpreced_def, fold the_preced_def, simp)
+thus ?thesis
+by (metis (no_types, lifting) cp_eq cpreced_def eq_dependants
+f_image_eq the_preced_def)
 qed
 text {*
 The following is another definition of @{term cp}.
 *}
 assumes "cs' \<noteq> cs"
 shows "wq (e#s) cs' = wq s cs'"
 using assms unfolding is_p wq_def
 by (auto simp:Let_def)
-lemma runing_th_s:
+lemma running_th_s:
-shows "th \<in> runing s"
+shows "th \<in> running s"
 proof -
 from pip_e[unfolded is_p]
 show ?thesis by (cases, simp)
 qed
 lemma th_not_in_wq:
 shows "th \<notin> set (wq s cs)"
 proof
 assume otherwise: "th \<in> set (wq s cs)"
-from runing_wqE[OF runing_th_s this]
+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)
 hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s"
 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,
-auto elim!:runing_wqE)
+auto elim!: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')"
 lemma threads_es [simp]: "threads (e#s) = threads s"
 by (unfold is_p, simp)
 lemma ready_th_s: "th \<in> readys s"
-using runing_th_s
+using running_th_s
-by (unfold runing_def, auto)
+by (unfold running_def, auto)
 lemma live_th_s: "th \<in> threads s"
 using readys_threads ready_th_s by auto
 lemma wq_threads_kept:
 proof -
 from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
 moreover then obtain cs where "n = Cs cs" by (unfold s_RAG_def, auto)
 ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
 hence "th \<in> set (wq s cs)"
-by (unfold s_RAG_def, auto simp:cs_waiting_raw)
+by (unfold s_RAG_def, auto simp: waiting_raw_def)
 from wq_threads [OF this] show ?thesis .
 qed
 lemma rg_RAG_threads:
 assumes "(Th th) \<in> Range (RAG s)"
 shows "th \<in> threads s"
 using assms
-by (unfold s_RAG_def cs_waiting_raw cs_holding_raw,
+unfolding s_RAG_def waiting_raw_def holding_raw_def
-auto intro:wq_threads)
+using wq_threads by auto
 lemma RAG_threads:
 assumes "(Th th) \<in> Field (RAG s)"
 shows "th \<in> threads s"
 using assms
 lemma th'_in_inv:
 assumes "th' \<in> set wq'"
 shows "th' \<in> set rest"
 using assms set_wq' by simp
-lemma runing_th_s:
+lemma running_th_s:
-shows "th \<in> runing s"
+shows "th \<in> running s"
 proof -
 from pip_e[unfolded is_v]
 show ?thesis by (cases, simp)
 qed
 next
 case False
 have "wq (e#s) c = wq s c" using False
 by simp
 hence "waiting s t c" using assms
-by (simp add: cs_waiting_raw waiting_eq)
+by (simp add: waiting_raw_def waiting_eq)
 hence "t \<notin> readys s" by (unfold readys_def, auto)
-hence "t \<notin> runing s" using runing_ready by auto
+hence "t \<notin> running s" using running_ready by auto
-with runing_th_s[folded otherwise] show ?thesis by auto
+with running_th_s[folded otherwise] show ?thesis by auto
 qed
 qed
 lemma waiting_esI1:
 assumes "waiting s t c"
 shows "waiting (e#s) t c"
 proof -
 have "wq (e#s) c = wq s c"
 using assms(2) by auto
 with assms(1) show ?thesis
-unfolding cs_waiting_raw waiting_eq by auto
+unfolding waiting_raw_def waiting_eq by auto
 qed
 lemma holding_esI2:
 assumes "c \<noteq> cs"
 and "holding s t c"
 by (simp add: distinct_rest)
 next
 fix x
 assume "distinct x \<and> set x = set rest"
 moreover have "t \<in> set rest"
-using assms(1) unfolding cs_waiting_raw waiting_eq wq_s_cs by auto
+using assms(1) unfolding waiting_raw_def waiting_eq wq_s_cs by auto
 ultimately show "t \<in> set x" by simp
 qed
 moreover have "t \<noteq> hd wq'"
 using assms(2) taker_def by auto
 ultimately show ?thesis
 obtains "c \<noteq> cs" "waiting s t c"
 |    "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'"
 proof(cases "c = cs")
 case False
 hence "wq (e#s) c = wq s c" by auto
-with assms have "waiting s t c" unfolding cs_waiting_raw waiting_eq by auto
+with assms have "waiting s t c" unfolding waiting_raw_def waiting_eq by auto
 from that(1)[OF False this] show ?thesis .
 next
 case True
 from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs]
 have "t \<noteq> hd wq'" "t \<in> set wq'" by auto
 hence "t \<noteq> taker" by (simp add: taker_def)
 moreover hence "t \<noteq> th" using assms neq_t_th by blast
 moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv)
 ultimately have "waiting s t cs"
-by (metis cs_waiting_raw insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs)
+by (metis waiting_raw_def insert_iff list.sel(1) s_waiting_abv set_simps(2) wq_def wq_s_cs)
 show ?thesis using that(2)
 using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto
 qed
 lemma holding_esI1:
 lemma waiting_esI2:
 assumes "waiting s t c"
 shows "waiting (e#s) t c"
 proof -
 have "c \<noteq> cs" using assms
-using rest_nil wq_s_cs unfolding cs_waiting_raw waiting_eq  by auto
+using rest_nil wq_s_cs unfolding waiting_raw_def waiting_eq  by auto
 from waiting_esI1[OF assms this]
 show ?thesis .
 qed
 lemma waiting_esE:
 assumes "waiting (e#s) t c"
 obtains "c \<noteq> cs" "waiting s t c"
 proof(cases "c = cs")
 case False
 hence "wq (e#s) c = wq s c"  by auto
-with assms have "waiting s t c" unfolding cs_waiting_raw waiting_eq by auto
+with assms have "waiting s t c" unfolding waiting_raw_def waiting_eq by auto
 from that(1)[OF False this] show ?thesis .
 next
 case True
 from no_waiter_after[OF assms[unfolded True]]
 show ?thesis by auto
 lemma waiting_kept:
 assumes "waiting s th' cs'"
 shows "waiting (e#s) th' cs'"
 using assms
-unfolding th_not_in_wq waiting_eq cs_waiting_raw
+unfolding th_not_in_wq waiting_eq waiting_raw_def
 by (metis append_is_Nil_conv butlast_snoc hd_append2 in_set_butlastD
 list.distinct(1) split_list wq_es_cs wq_neq_simp)
 lemma holding_kept:
 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 cs_holding_raw holding_eq by auto
+with assms show ?thesis unfolding holding_raw_def holding_eq 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: cs_holding_raw holding_eq)
+by (simp add: holding_raw_def holding_eq)
 qed
 end
 lemma (in valid_trace_p) th_not_waiting: "\<not> waiting s th c"
 proof -
 have "th \<in> readys s"
-using runing_ready runing_th_s by blast
+using running_ready running_th_s by blast
 thus ?thesis
 by (unfold readys_def, auto)
 qed
 context valid_trace_p_h
 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 cs_holding_raw holding_eq by blast
+thus ?thesis unfolding holding_raw_def holding_eq 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)
 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 cs_holding_raw holding_eq by auto
+using False unfolding holding_raw_def holding_eq 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)
 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 unfolding cs_waiting_raw by auto
+using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs unfolding waiting_raw_def 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)
 lemma holding_esE:
 using assms
 proof(cases "cs' = cs")
 case False
 hence "wq (e#s) cs' = wq s cs'" by simp
 with assms show ?thesis using that
-unfolding cs_holding_raw holding_eq by auto
+unfolding holding_raw_def holding_eq by auto
 next
 case True
 with assms show ?thesis
 using s_holding_def that wq_def wq_es_cs' wq_s_cs by auto
 qed
 qed
 from that(1)[OF this True] show ?thesis .
 next
 case False
 hence "th' = th \<and> cs' = cs"
-by (metis assms cs_waiting_raw holder_def list.sel(1) rotate1.simps(2)
+by (metis assms waiting_raw_def holder_def list.sel(1) rotate1.simps(2)
 set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp)
 with that(2) show ?thesis by metis
 qed
 lemma RAG_es: "RAG (e # s) =  RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R")
 lemma finite_RAG:
 shows "finite (RAG s)"
 proof(induct rule:ind)
 case Nil
 show ?case
-by (auto simp: s_RAG_def cs_waiting_raw
+by (auto simp: s_RAG_def waiting_raw_def
-cs_holding_raw wq_def acyclic_def)
+holding_raw_def wq_def acyclic_def)
 next
 case (Cons s e)
 interpret vt_e: valid_trace_e s e using Cons by simp
 show ?case
 proof(cases e)
 lemma acyclic_RAG:
 shows "acyclic (RAG s)"
 proof(induct rule:ind)
 case Nil
 show ?case
-by (auto simp: s_RAG_def cs_waiting_raw
+by (auto simp: s_RAG_def waiting_raw_def
-cs_holding_raw wq_def acyclic_def)
+holding_raw_def wq_def acyclic_def)
 next
 case (Cons s e)
 interpret vt_e: valid_trace_e s e using Cons by simp
 show ?case
 proof(cases e)
 case True
 thus ?thesis by auto
 next
 case False
 from False and th_in have "Th th \<in> Domain (RAG s)"
-by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_raw Domain_def)
+by (auto simp: readys_def s_waiting_def s_RAG_def wq_def waiting_raw_def
+Domain_def)
 from chain_building [rule_format, OF this]
 show ?thesis by auto
 qed
 text {*
 text {*
 The following two lemmas shows there is at most one running thread
 in the system.
 *}
-lemma runing_unique:
+lemma running_unique:
-assumes runing_1: "th1 \<in> runing s"
+assumes running_1: "th1 \<in> running s"
-and runing_2: "th2 \<in> runing s"
+and running_2: "th2 \<in> running s"
 shows "th1 = th2"
 proof -
-from runing_1 and runing_2 have "cp s th1 = cp s th2"
+from running_1 and running_2 have "cp s th1 = cp s th2"
-unfolding runing_def by auto
+unfolding running_def by auto
 from this[unfolded cp_alt_def]
 have eq_max:
 "Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) =
 Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th2)})"
 (is "Max ?L = Max ?R") .
 from h_1(1)
 show "th1' \<in> threads s"
 proof(cases rule:subtreeE)
 case 1
 hence "th1' = th1" by simp
-with runing_1 show ?thesis by (auto simp:runing_def readys_def)
+with running_1 show ?thesis by (auto simp:running_def readys_def)
 next
 case 2
 from this(2)
 have "(Th th1', Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)
 from tranclD[OF this]
 from h_2(1)
 show "th2' \<in> threads s"
 proof(cases rule:subtreeE)
 case 1
 hence "th2' = th2" by simp
-with runing_2 show ?thesis by (auto simp:runing_def readys_def)
+with running_2 show ?thesis by (auto simp:running_def readys_def)
 next
 case 2
 from this(2)
 have "(Th th2', Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)
 from tranclD[OF this]
 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)
-with runing_1 show False
+with running_1 show False
-by (unfold runing_def readys_def, auto)
+by (unfold running_def readys_def, auto)
 qed
 ultimately have "xs2 = xs1" by simp
 from rpath_dest_eq[OF rp1 rp2[unfolded this]]
 show ?thesis by simp
 next
 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)
-with runing_2 show False
+with running_2 show False
-by (unfold runing_def readys_def, auto)
+by (unfold running_def readys_def, auto)
 qed
 ultimately have "xs2 = xs1" by simp
 from rpath_dest_eq[OF rp1 rp2[unfolded this]]
 show ?thesis by simp
 qed
 qed
-lemma card_runing: "card (runing s) \<le> 1"
+lemma card_running: "card (running s) \<le> 1"
-proof(cases "runing s = {}")
+proof(cases "running s = {}")
 case True
 thus ?thesis by auto
 next
 case False
-then obtain th where [simp]: "th \<in> runing s" by auto
+then obtain th where [simp]: "th \<in> running s" by auto
-from runing_unique[OF this]
+from running_unique[OF this]
-have "runing s = {th}" by auto
+have "running s = {th}" by auto
 thus ?thesis by auto
 qed
 text {*
 The following two lemmas show that the set of living threads
 show False
 proof(cases)
 case (thread_P)
 moreover have "(Cs cs, Th th) \<in> RAG s"
 using otherwise th_not_in_wq
-unfolding cs_holding_raw holding_eq  by auto
+unfolding holding_raw_def holding_eq  by auto
 ultimately show ?thesis by auto
 qed
 qed
 lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1"
 lemma holding_th_cs_s:
 "holding s th cs"
 by  (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
 lemma th_ready_s [simp]: "th \<in> readys s"
-using runing_th_s
+using running_th_s
-by (unfold runing_def readys_def, auto)
+by (unfold running_def readys_def, auto)
 lemma th_live_s [simp]: "th \<in> threads s"
 using th_ready_s by (unfold readys_def, auto)
 lemma th_ready_es [simp]: "th \<in> readys (e#s)"
-using runing_th_s neq_t_th
+using running_th_s neq_t_th
-by (unfold is_v runing_def readys_def, auto)
+by (unfold is_v running_def readys_def, auto)
 lemma th_live_es [simp]: "th \<in> threads (e#s)"
 using th_ready_es by (unfold readys_def, auto)
 lemma pvD_th_s[simp]: "pvD s th = 0"
 lemma th_not_waiting:
 "\<not> waiting s th c"
 proof -
 have "th \<in> readys s"
-using runing_ready runing_th_s by blast
+using running_ready running_th_s by blast
 thus ?thesis
 by (unfold readys_def, auto)
 qed
 lemma waiting_neq_th:
 lemma th_live_s [simp]: "th \<in> threads s"
 proof -
 from pip_e[unfolded is_exit]
 show ?thesis
-by (cases, unfold runing_def readys_def, simp)
+by (cases, unfold running_def readys_def, simp)
 qed
 lemma th_ready_s [simp]: "th \<in> readys s"
 proof -
 from pip_e[unfolded is_exit]
 show ?thesis
-by (cases, unfold runing_def, simp)
+by (cases, unfold running_def, simp)
 qed
 lemma th_not_live_es [simp]: "th \<notin> threads (e#s)"
 by (unfold is_exit, simp)
 lemma th_live_s [simp]: "th \<in> threads s"
 proof -
 from pip_e[unfolded is_set]
 show ?thesis
-by (cases, unfold runing_def readys_def, simp)
+by (cases, unfold running_def readys_def, simp)
 qed
 lemma th_ready_s [simp]: "th \<in> readys s"
 proof -
 from pip_e[unfolded is_set]
 show ?thesis
-by (cases, unfold runing_def, simp)
+by (cases, unfold running_def, simp)
 qed
 lemma th_not_live_es [simp]: "th \<in> threads (e#s)"
 by (unfold is_set, simp)
 lemma PIP_actorE:
 assumes "PIP s e"
 and "actor e = th"
 and "\<not> isCreate e"
-shows "th \<in> runing s"
+shows "th \<in> running s"
 using assms
 by (cases, auto)
 lemma holdents_RAG:
 proof(rule RangeE)
 fix a
 assume "(a, Th th) \<in> RAG s"
 with assms[unfolded holdents_test]
 show False
-by (cases a, auto simp:cs_RAG_raw s_RAG_abv)
+by (cases a, auto simp:RAG_raw_def s_RAG_abv)
 qed
 qed
 lemma readys_RAG:
 assumes "th \<in> readys s"
 proof(rule DomainE)
 fix b
 assume "(Th th, b) \<in> RAG s"
 with assms[unfolded readys_def s_waiting_def]
 show False
-by (cases b, auto simp:cs_RAG_raw s_RAG_abv cs_waiting_raw)
+by (cases b, auto simp: RAG_raw_def s_RAG_abv waiting_raw_def)
 qed
 qed
 lemma readys_holdents_detached:
 assumes "th \<in> readys s"

changeset 127	38c6acf03f68
parent 125	95e7933968f8
child 128	5d8ec128518b