--- a/PIPBasics.thy Tue Jun 07 13:51:39 2016 +0100
+++ b/PIPBasics.thy Thu Jun 09 23:01:36 2016 +0100
@@ -3,15 +3,15 @@
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
- the correctness of this model, we are going to derive a series of
- expected properties out of it.
-
- This file contains the very basic properties, useful for self-assurance,
- as well as for deriving more advance properties concerning
- the correctness and implementation of PIP.
-*}
+ given a concise and miniature model of PIP. To assure ourselves of the
+ correctness of this model, we are going to derive a series of expected
+ properties out of it.
+
+ This file contains the very basic properties, useful for self-assurance,
+ as well as for deriving more advance properties concerning the correctness
+ and implementation of PIP. *}
section {* Generic auxiliary lemmas *}
@@ -135,9 +135,10 @@
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"
@@ -150,33 +151,6 @@
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
@@ -205,12 +179,12 @@
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:
- shows "runing s \<subseteq> readys s"
- unfolding runing_def readys_def
+lemma running_ready:
+ shows "running s \<subseteq> readys s"
+ unfolding running_def readys_def
by auto
lemma readys_threads:
@@ -224,8 +198,8 @@
In other words, a running thread must have got every
resource it has requested.
*}
-lemma runing_wqE:
- assumes "th \<in> runing s"
+lemma running_wqE:
+ assumes "th \<in> running s"
and "th \<in> set (wq s cs)"
obtains rest where "wq s cs = th#rest"
proof -
@@ -239,7 +213,7 @@
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
@@ -391,9 +365,6 @@
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
@@ -597,18 +568,22 @@
are in place.
*}
lemma cp_alt_def:
- "cp s th =
- Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
+ "cp s th = Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
proof -
- have "Max (the_preced s ` ({th} \<union> dependants_raw (wq s) th)) =
+ have "Max (the_preced s ` ({th} \<union> dependants 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 {*
@@ -1060,8 +1035,8 @@
using assms unfolding is_p wq_def
by (auto simp:Let_def)
-lemma runing_th_s:
- shows "th \<in> runing s"
+lemma running_th_s:
+ shows "th \<in> running s"
proof -
from pip_e[unfolded is_p]
show ?thesis by (cases, simp)
@@ -1071,7 +1046,7 @@
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"
@@ -1254,7 +1229,7 @@
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:
@@ -1350,8 +1325,8 @@
by (unfold is_p, simp)
lemma ready_th_s: "th \<in> readys s"
- using runing_th_s
- by (unfold runing_def, auto)
+ using running_th_s
+ by (unfold running_def, auto)
lemma live_th_s: "th \<in> threads s"
using readys_threads ready_th_s by auto
@@ -1474,7 +1449,7 @@
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
@@ -1482,8 +1457,8 @@
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,
- auto intro:wq_threads)
+ unfolding s_RAG_def waiting_raw_def holding_raw_def
+using wq_threads by auto
lemma RAG_threads:
assumes "(Th th) \<in> Field (RAG s)"
@@ -1593,8 +1568,8 @@
shows "th' \<in> set rest"
using assms set_wq' by simp
-lemma runing_th_s:
- shows "th \<in> runing s"
+lemma running_th_s:
+ shows "th \<in> running s"
proof -
from pip_e[unfolded is_v]
show ?thesis by (cases, simp)
@@ -1619,10 +1594,10 @@
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
- with runing_th_s[folded otherwise] show ?thesis by auto
+ hence "t \<notin> running s" using running_ready by auto
+ with running_th_s[folded otherwise] show ?thesis by auto
qed
qed
@@ -1634,7 +1609,7 @@
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:
@@ -1722,7 +1697,7 @@
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'"
@@ -1738,7 +1713,7 @@
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
@@ -1748,7 +1723,7 @@
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
@@ -1845,7 +1820,7 @@
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
@@ -1856,7 +1831,7 @@
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
@@ -2077,7 +2052,7 @@
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)
@@ -2087,7 +2062,7 @@
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]
@@ -2096,14 +2071,14 @@
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
@@ -2119,7 +2094,7 @@
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)"
@@ -2144,7 +2119,7 @@
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
@@ -2214,7 +2189,7 @@
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)
@@ -2227,7 +2202,7 @@
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
@@ -2250,7 +2225,7 @@
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
@@ -2361,8 +2336,8 @@
proof(induct rule:ind)
case Nil
show ?case
- by (auto simp: s_RAG_def cs_waiting_raw
- cs_holding_raw wq_def acyclic_def)
+ by (auto simp: s_RAG_def waiting_raw_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
@@ -2794,8 +2769,8 @@
proof(induct rule:ind)
case Nil
show ?case
- by (auto simp: s_RAG_def cs_waiting_raw
- cs_holding_raw wq_def acyclic_def)
+ by (auto simp: s_RAG_def waiting_raw_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
@@ -3084,7 +3059,8 @@
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
@@ -3115,13 +3091,13 @@
The following two lemmas shows there is at most one running thread
in the system.
*}
-lemma runing_unique:
- assumes runing_1: "th1 \<in> runing s"
- and runing_2: "th2 \<in> runing s"
+lemma running_unique:
+ assumes running_1: "th1 \<in> running 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"
- unfolding runing_def by auto
+ from running_1 and running_2 have "cp s th1 = cp s th2"
+ 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)}) =
@@ -3152,7 +3128,7 @@
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)
@@ -3167,7 +3143,7 @@
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)
@@ -3203,8 +3179,8 @@
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
- by (unfold runing_def readys_def, 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]]
@@ -3219,8 +3195,8 @@
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
- by (unfold runing_def readys_def, 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]]
@@ -3228,15 +3204,15 @@
qed
qed
-lemma card_runing: "card (runing s) \<le> 1"
-proof(cases "runing s = {}")
+lemma card_running: "card (running s) \<le> 1"
+proof(cases "running s = {}")
case True
thus ?thesis by auto
next
case False
- then obtain th where [simp]: "th \<in> runing s" by auto
- from runing_unique[OF this]
- have "runing s = {th}" by auto
+ then obtain th where [simp]: "th \<in> running s" by auto
+ from running_unique[OF this]
+ have "running s = {th}" by auto
thus ?thesis by auto
qed
@@ -3635,7 +3611,7 @@
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
@@ -3819,15 +3795,15 @@
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
- by (unfold runing_def readys_def, auto)
+ using running_th_s
+ 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
- by (unfold is_v runing_def readys_def, auto)
+ using running_th_s neq_t_th
+ 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)
@@ -3858,7 +3834,7 @@
"\<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
@@ -4478,14 +4454,14 @@
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)"
@@ -4625,14 +4601,14 @@
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)"
@@ -5111,7 +5087,7 @@
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)
@@ -5127,7 +5103,7 @@
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
@@ -5142,7 +5118,7 @@
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