pip: comparison PrioG.thy

equal deleted inserted replaced

-:031d2ae9c9b8
+:b620a2a0806a
 theory PrioG
 imports PrioGDef
 begin
+locale valid_trace =
+fixes s
+assumes vt : "vt s"
+locale valid_trace_e = valid_trace +
+fixes e
+assumes vt_e: "vt (e#s)"
+begin
+lemma pip_e: "PIP s e"
+using vt_e by (cases, simp)
+end
 lemma runing_ready:
 shows "runing s \<subseteq> readys s"
 unfolding runing_def readys_def
 by auto
 lemma wq_v_neq:
 "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"
 by (auto simp:wq_def Let_def cp_def split:list.splits)
-lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"
+context valid_trace
-proof(erule_tac vt.induct, simp add:wq_def)
+begin
+lemma ind [consumes 0, case_names Nil Cons, induct type]:
+assumes "PP []"
+and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow>
+PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"
+shows "PP s"
+proof(rule vt.induct[OF vt])
+from assms(1) show "PP []" .
+next
+fix s e
+assume h: "vt s" "PP s" "PIP s e"
+show "PP (e # s)"
+proof(cases rule:assms(2))
+from h(1) show v1: "valid_trace s" by (unfold_locales, simp)
+next
+from h(1,3) have "vt (e#s)" by auto
+thus "valid_trace (e # s)" by (unfold_locales, simp)
+qed (insert h, auto)
+qed
+lemma wq_distinct: "distinct (wq s cs)"
+proof(rule ind, simp add:wq_def)
 fix s e
 assume h1: "step s e"
 and h2: "distinct (wq s cs)"
 thus "distinct (wq (e # s) cs)"
 proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)
 thus "distinct q" by auto
 qed
 qed
 qed
+end
+context valid_trace_e
+begin
 text {*
 The following lemma shows that only the @{text "P"}
 operation can add new thread into waiting queues.
 Such kind of lemmas are very obvious, but need to be checked formally.
 This is a kind of confirmation that our modelling is correct.
 *}
 lemma block_pre:
-fixes thread cs s
+assumes s_ni: "thread \<notin>  set (wq s cs)"
-assumes vt_e: "vt (e#s)"
-and s_ni: "thread \<notin>  set (wq s cs)"
 and s_i: "thread \<in> set (wq (e#s) cs)"
 shows "e = P thread cs"
 proof -
 show ?thesis
 proof(cases e)
 case (Set th prio)
 with assms show ?thesis
 by (auto simp:wq_def Let_def split:if_splits)
 next
 case (V th cs)
-with assms show ?thesis
+with vt_e assms show ?thesis
 apply (auto simp:wq_def Let_def split:if_splits)
 proof -
 fix q qs
 assume h1: "thread \<notin> set (wq_fun (schs s) cs)"
 and h2: "q # qs = wq_fun (schs s) cs"
 from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
 moreover have "thread \<in> set qs"
 proof -
 have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
 proof(rule someI2)
-from wq_distinct [OF step_back_vt[OF vt], of cs]
+from wq_distinct [of cs]
 and h2[symmetric, folded wq_def]
 show "distinct qs \<and> set qs = set qs" by auto
 next
 fix x assume "distinct x \<and> set x = set qs"
 thus "set x = set qs" by auto
 ultimately show "False" by auto
 qed
 qed
 qed
+end
 text {*
 The following lemmas is also obvious and shallow. It says
 that only running thread can request for a critical resource
 and that the requested resource must be one which is
 not current held by the thread.
 apply (ind_cases "vt ((P thread cs)#s)")
 apply (ind_cases "step s (P thread cs)")
 by auto
 lemma abs1:
-fixes e es
 assumes ein: "e \<in> set es"
 and neq: "hd es \<noteq> hd (es @ [x])"
 shows "False"
 proof -
 from ein have "es \<noteq> []" by auto
 lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"
 by (cases es, auto)
 inductive_cases evt_cons: "vt (a#s)"
+context valid_trace_e
+begin
 lemma abs2:
-assumes vt: "vt (e#s)"
+assumes inq: "thread \<in> set (wq s cs)"
-and inq: "thread \<in> set (wq s cs)"
 and nh: "thread = hd (wq s cs)"
 and qt: "thread \<noteq> hd (wq (e#s) cs)"
 and inq': "thread \<in> set (wq (e#s) cs)"
 shows "False"
 proof -
-from assms show "False"
+from vt_e assms show "False"
 apply (cases e)
 apply ((simp split:if_splits add:Let_def wq_def)[1])+
 apply (insert abs1, fast)[1]
 apply (auto simp:wq_def simp:Let_def split:if_splits list.splits)
 proof -
 assume vt: "vt (V th cs # s)"
 and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
 and eq_wq: "wq_fun (schs s) cs = thread # qs"
 show "False"
 proof -
-from wq_distinct[OF step_back_vt[OF vt], of cs]
+from wq_distinct[of cs]
 and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp
 moreover have "thread \<in> set qs"
 proof -
 have "set (SOME q. distinct q \<and> set q = set qs) = set qs"
 proof(rule someI2)
-from wq_distinct [OF step_back_vt[OF vt], of cs]
+from wq_distinct [of cs]
 and eq_wq [folded wq_def]
 show "distinct qs \<and> set qs = set qs" by auto
 next
 fix x assume "distinct x \<and> set x = set qs"
 thus "set x = set qs" by auto
 ultimately show ?thesis by auto
 qed
 qed
 qed
-lemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
+end
-proof(induct s, simp)
-fix a s t
+context valid_trace
-assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"
+begin
-and vt_a: "vt (a # s)"
-show "vt (moment t (a # s))"
+lemma vt_moment: "\<And> t. vt (moment t s)"
-proof(cases "t \<ge> length (a#s)")
+proof(induct rule:ind)
+case Nil
+thus ?case by (simp add:vt_nil)
+next
+case (Cons s e t)
+show ?case
+proof(cases "t \<ge> length (e#s)")
 case True
-from True have "moment t (a#s) = a#s" by simp
+from True have "moment t (e#s) = e#s" by simp
-with vt_a show ?thesis by simp
+thus ?thesis using Cons
+by (simp add:valid_trace_def)
 next
 case False
-hence le_t1: "t \<le> length s" by simp
+from Cons have "vt (moment t s)" by simp
-from vt_a have "vt s"
+moreover have "moment t (e#s) = moment t s"
-by (erule_tac evt_cons, simp)
-from h [OF this] have "vt (moment t s)" .
-moreover have "moment t (a#s) = moment t s"
 proof -
-from moment_app [OF le_t1, of "[a]"]
+from False have "t \<le> length s" by simp
+from moment_app [OF this, of "[e]"]
 show ?thesis by simp
 qed
-ultimately show ?thesis by auto
+ultimately show ?thesis by simp
 qed
 qed
 (* Wrong:
 lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
 in blocked state at moment @{text "t2"} and could not
 make any request and get blocked the second time: Contradiction.
 *}
 lemma waiting_unique_pre:
-fixes cs1 cs2 s thread
+assumes h11: "thread \<in> set (wq s cs1)"
-assumes vt: "vt s"
-and h11: "thread \<in> set (wq s cs1)"
 and h12: "thread \<noteq> hd (wq s cs1)"
 assumes h21: "thread \<in> set (wq s cs2)"
 and h22: "thread \<noteq> hd (wq s cs2)"
 and neq12: "cs1 \<noteq> cs2"
 shows "False"
 obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto
 have "t2 < ?t3" by simp
 from nn2 [rule_format, OF this] and eq_m
 have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
 h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto
-have vt_e: "vt (e#moment t2 s)"
+have "vt (e#moment t2 s)"
 proof -
-from vt_moment [OF vt]
+from vt_moment
 have "vt (moment ?t3 s)" .
 with eq_m show ?thesis by simp
 qed
+then interpret vt_e: valid_trace_e "moment t2 s" "e"
+by (unfold_locales, auto, cases, simp)
 have ?thesis
 proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
 case True
 from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
 by auto
-thm abs2
+from vt_e.abs2 [OF True eq_th h2 h1]
-from abs2 [OF vt_e True eq_th h2 h1]
 show ?thesis by auto
 next
 case False
-from block_pre [OF vt_e False h1]
+from vt_e.block_pre[OF False h1]
 have "e = P thread cs2" .
-with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
+with vt_e.vt_e have "vt ((P thread cs2)# moment t2 s)" by simp
 from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp
 with runing_ready have "thread \<in> readys (moment t2 s)" by auto
 with nn1 [rule_format, OF lt12]
 show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)
 qed
 obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto
 have lt_t3: "t1 < ?t3" by simp
 from nn1 [rule_format, OF this] and eq_m
 have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
 h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
-have vt_e: "vt  (e#moment t1 s)"
+have "vt  (e#moment t1 s)"
 proof -
-from vt_moment [OF vt]
+from vt_moment
 have "vt (moment ?t3 s)" .
 with eq_m show ?thesis by simp
 qed
+then interpret vt_e: valid_trace_e "moment t1 s" e
+by (unfold_locales, auto, cases, auto)
 have ?thesis
 proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
 case True
 from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
 by auto
-from abs2 [OF vt_e True eq_th h2 h1]
+from vt_e.abs2 True eq_th h2 h1
 show ?thesis by auto
 next
 case False
-from block_pre [OF vt_e False h1]
+from vt_e.block_pre [OF False h1]
 have "e = P thread cs1" .
-with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
+with vt_e.vt_e have "vt ((P thread cs1)# moment t1 s)" by simp
 from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp
 with runing_ready have "thread \<in> readys (moment t1 s)" by auto
 with nn2 [rule_format, OF lt12]
 show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)
 qed
 from nn1 [rule_format, OF this] and eq_m
 have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
 h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto
 have vt_e: "vt (e#moment t1 s)"
 proof -
-from vt_moment [OF vt]
+from vt_moment
 have "vt (moment ?t3 s)" .
 with eq_m show ?thesis by simp
 qed
+then interpret vt_e: valid_trace_e "moment t1 s" e
+by (unfold_locales, auto, cases, auto)
 have ?thesis
 proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
 case True
 from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"
 by auto
-from abs2 [OF vt_e True eq_th h2 h1]
+from vt_e.abs2 [OF True eq_th h2 h1]
 show ?thesis by auto
 next
 case False
-from block_pre [OF vt_e False h1]
+from vt_e.block_pre [OF False h1]
 have eq_e1: "e = P thread cs1" .
 have lt_t3: "t1 < ?t3" by simp
 with eqt12 have "t2 < ?t3" by simp
 from nn2 [rule_format, OF this] and eq_m and eqt12
 have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and
 proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
 case True
 from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"
 by auto
 from vt_e and eqt12 have "vt (e#moment t2 s)" by simp
-from abs2 [OF this True eq_th h2 h1]
+then interpret vt_e2: valid_trace_e "moment t2 s" e
+by (unfold_locales, auto, cases, auto)
+from vt_e2.abs2 [OF True eq_th h2 h1]
 show ?thesis .
 next
 case False
-have vt_e: "vt (e#moment t2 s)"
+have "vt (e#moment t2 s)"
 proof -
-from vt_moment [OF vt] eqt12
+from vt_moment eqt12
 have "vt (moment (Suc t2) s)" by auto
 with eq_m eqt12 show ?thesis by simp
 qed
-from block_pre [OF vt_e False h1]
+then interpret vt_e2: valid_trace_e "moment t2 s" e
+by (unfold_locales, auto, cases, auto)
+from vt_e2.block_pre [OF False h1]
 have "e = P thread cs2" .
 with eq_e1 neq12 show ?thesis by auto
 qed
 qed
 } ultimately show ?thesis by arith
 text {*
 This lemma is a simple corrolary of @{text "waiting_unique_pre"}.
 *}
 lemma waiting_unique:
-fixes s cs1 cs2
+assumes "waiting s th cs1"
-assumes "vt s"
-and "waiting s th cs1"
 and "waiting s th cs2"
 shows "cs1 = cs2"
 using waiting_unique_pre assms
 unfolding wq_def s_waiting_def
 by auto
+end
 (* not used *)
 text {*
 Every thread can only be blocked on one critical resource,
 symmetrically, every critical resource can only be held by one thread.
 This fact is much more easier according to our definition.
 *}
 lemma held_unique:
-fixes s::"state"
+assumes "holding (s::event list) th1 cs"
-assumes "holding s th1 cs"
 and "holding s th2 cs"
 shows "th1 = th2"
-using assms
+by (insert assms, unfold s_holding_def, auto)
-unfolding s_holding_def
-by auto
 lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
 apply (induct s, auto)
 by (case_tac a, auto split:if_splits)
 proof -
 fix t c
 assume vt: "vt (V th cs # s)"
 and nw: "\<not> waiting (wq (V th cs # s)) t c"
 and wt: "waiting (wq s) t c"
+from vt interpret vt_v: valid_trace_e s "V th cs"
+by  (cases, unfold_locales, simp)
 show "next_th s th cs t \<and> cs = c"
 proof(cases "cs = c")
 case False
 with nw wt show ?thesis
 by (auto simp:cs_waiting_def wq_def Let_def)
 assume t_in: "t \<in> set list"
 and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
 and eq_wq: "wq_fun (schs s) cs = a # list"
 have " set (SOME q. distinct q \<and> set q = set list) = set list"
 proof(rule someI2)
-from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
 show "distinct list \<and> set list = set list" by auto
 next
 show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
 by auto
 qed
 assume t_in: "t \<in> set list"
 and t_ni: "t \<notin> set (SOME q. distinct q \<and> set q = set list)"
 and eq_wq: "wq_fun (schs s) cs = a # list"
 have " set (SOME q. distinct q \<and> set q = set list) = set list"
 proof(rule someI2)
-from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq[folded wq_def]
+from vt_v.wq_distinct[of cs] and eq_wq[folded wq_def]
 show "distinct list \<and> set list = set list" by auto
 next
 show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
 by auto
 qed
 lemma step_v_release:
 "\<lbrakk>vt (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
 proof -
 assume vt: "vt (V th cs # s)"
 and hd: "holding (wq (V th cs # s)) th cs"
+from vt interpret vt_v: valid_trace_e s "V th cs"
+by (cases, unfold_locales, simp+)
 from step_back_step [OF vt] and hd
 show "False"
 proof(cases)
 assume "holding (wq (V th cs # s)) th cs" and "holding s th cs"
 thus ?thesis
 "wq_fun (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list"
 and hd_in: "hd (SOME q. distinct q \<and> set q = set list)
 \<in> set (SOME q. distinct q \<and> set q = set list)"
 have "set (SOME q. distinct q \<and> set q = set list) = set list"
 proof(rule someI2)
-from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+from vt_v.wq_distinct[of cs] and eq_wq
 show "distinct list \<and> set list = set list" by auto
 next
 show "\<And>x. distinct x \<and> set x = set list \<Longrightarrow> set x = set list"
 by auto
 qed
 moreover have "distinct  (hd (SOME q. distinct q \<and> set q = set list) # list)"
 proof -
-from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+from vt_v.wq_distinct[of cs] and eq_wq
 show ?thesis by auto
 qed
 moreover note eq_wq and hd_in
 ultimately show "False" by auto
 qed
 assume vt: "vt (V th cs # s)"
 and eq_wq[folded wq_def]: " wq_fun (schs s) cs = th # rest"
 and nrest: "rest \<noteq> []"
 and ni: "hd (SOME q. distinct q \<and> set q = set rest)
 \<notin> set (SOME q. distinct q \<and> set q = set rest)"
+from vt interpret vt_v: valid_trace_e s "V th cs"
+by (cases, unfold_locales, simp+)
 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 proof(rule someI2)
-from wq_distinct[OF step_back_vt[OF vt], of cs] and eq_wq
+from vt_v.wq_distinct[of cs] and eq_wq
 show "distinct rest \<and> set rest = set rest" by auto
 next
 fix x assume "distinct x \<and> set x = set rest"
 hence "set x = set rest" by auto
 with nrest
 proof -
 fix t c
 let ?s' = "(V th cs # s)"
 assume vt: "vt ?s'"
 and wt: "waiting (wq ?s') t c"
+from vt interpret vt_v: valid_trace_e s "V th cs"
+by (cases, unfold_locales, simp+)
 show "waiting (wq s) t c"
 proof(cases "c = cs")
 case False
 assume neq_cs: "c \<noteq> cs"
 hence "waiting (wq ?s') t c = waiting (wq s) t c"
 assume not_in: "t \<notin> set list"
 and is_in: "t \<in> set (SOME q. distinct q \<and> set q = set list)"
 and eq_wq: "wq_fun (schs s) cs = a # list"
 have "set (SOME q. distinct q \<and> set q = set list) = set list"
 proof(rule someI2)
-from wq_distinct [OF step_back_vt[OF vt], of cs]
+from vt_v.wq_distinct [of cs]
 and eq_wq[folded wq_def]
 show "distinct list \<and> set list = set list" by auto
 next
 fix x assume "distinct x \<and> set x = set list"
 thus "set x = set list" by auto
 apply (unfold wq_def, auto simp:Let_def cs_waiting_def)
 proof -
 assume " t \<in> set (SOME q. distinct q \<and> set q = set list)"
 moreover have "\<dots> = set list"
 proof(rule someI2)
-from wq_distinct [OF step_back_vt[OF vt], of cs]
+from vt_v.wq_distinct [of cs]
 and eq_wq[folded wq_def]
 show "distinct list \<and> set list = set list" by auto
 next
 fix x assume "distinct x \<and> set x = set list"
 thus "set x = set list" by auto
 qed
 ultimately show "t \<in> set list" by simp
 qed
-with eq_wq and wq_distinct [OF step_back_vt[OF vt], of cs, unfolded wq_def]
+with eq_wq and vt_v.wq_distinct [of cs, unfolded wq_def]
 show False by auto
 qed
 qed
 qed
 lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
 by (unfold s_RAG_def, auto)
+context valid_trace
+begin
 text {*
 The following lemma shows that @{text "RAG"} is acyclic.
 The overall structure is by induction on the formation of @{text "vt s"}
 and then case analysis on event @{text "e"}, where the non-trivial cases
 for those for @{text "V"} and @{text "P"} events.
 *}
 lemma acyclic_RAG:
-fixes s
-assumes vt: "vt s"
 shows "acyclic (RAG s)"
-using assms
+using vt
 proof(induct)
 case (vt_cons s e)
+interpret vt_s: valid_trace s using vt_cons(1)
+by (unfold_locales, simp)
 assume ih: "acyclic (RAG s)"
 and stp: "step s e"
 and vt: "vt s"
 show ?case
 proof(cases e)
 obtain cs' where eq_x: "x = Cs cs'" by auto
 with th_d have "(Th ?th', Cs cs') \<in> ?A" by simp
 hence wt_th': "waiting s ?th' cs'"
 unfolding s_RAG_def s_waiting_def cs_waiting_def wq_def by simp
 hence "cs' = cs"
-proof(rule waiting_unique [OF vt])
+proof(rule vt_s.waiting_unique)
-from eq_wq wq_distinct[OF vt, of cs]
+from eq_wq vt_s.wq_distinct[of cs]
 show "waiting s ?th' cs"
 apply (unfold s_waiting_def wq_def, auto)
 proof -
 assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
 and eq_wq: "wq_fun (schs s) cs = th # rest"
 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 proof(rule someI2)
-from wq_distinct[OF vt, of cs] and eq_wq
+from vt_s.wq_distinct[of cs] and eq_wq
 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
 next
 fix x assume "distinct x \<and> set x = set rest"
 with False show "x \<noteq> []" by auto
 qed
 hence "hd (SOME q. distinct q \<and> set q = set rest) \<in>
 set (SOME q. distinct q \<and> set q = set rest)" by auto
 moreover have "\<dots> = set rest"
 proof(rule someI2)
-from wq_distinct[OF vt, of cs] and eq_wq
+from vt_s.wq_distinct[of cs] and eq_wq
 show "distinct rest \<and> set rest = set rest" unfolding wq_def by auto
 next
 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 qed
 moreover note hd_in
 next
 assume hd_in: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
 and eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"
 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 proof(rule someI2)
-from wq_distinct[OF vt, of cs] and eq_wq
+from vt_s.wq_distinct[of cs] and eq_wq
 show "distinct rest \<and> set rest = set rest" by auto
 next
 fix x assume "distinct x \<and> set x = set rest"
 with False show "x \<noteq> []" by auto
 qed
 hence "hd (SOME q. distinct q \<and> set q = set rest) \<in>
 set (SOME q. distinct q \<and> set q = set rest)" by auto
 moreover have "\<dots> = set rest"
 proof(rule someI2)
-from wq_distinct[OF vt, of cs] and eq_wq
+from vt_s.wq_distinct[of cs] and eq_wq
 show "distinct rest \<and> set rest = set rest" by auto
 next
 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 qed
 moreover note hd_in
 by (auto simp: s_RAG_def cs_waiting_def
 cs_holding_def wq_def acyclic_def)
 qed
 lemma finite_RAG:
-fixes s
-assumes vt: "vt s"
 shows "finite (RAG s)"
 proof -
 from vt show ?thesis
 proof(induct)
 case (vt_cons s e)
+interpret vt_s: valid_trace s using vt_cons(1)
+by (unfold_locales, simp)
 assume ih: "finite (RAG s)"
 and stp: "step s e"
 and vt: "vt s"
 show ?case
 proof(cases e)
 qed
 text {* Several useful lemmas *}
 lemma wf_dep_converse:
-fixes s
-assumes vt: "vt s"
 shows "wf ((RAG s)^-1)"
 proof(rule finite_acyclic_wf_converse)
-from finite_RAG [OF vt]
+from finite_RAG
 show "finite (RAG s)" .
 next
-from acyclic_RAG[OF vt]
+from acyclic_RAG
 show "acyclic (RAG s)" .
 qed
+end
 lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
 by (induct l, auto)
 lemma th_chasing: "(Th th, Cs cs) \<in> RAG (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> RAG s"
 by (auto simp:s_RAG_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
+context valid_trace
+begin
 lemma wq_threads:
-fixes s cs
+assumes h: "th \<in> set (wq s cs)"
-assumes vt: "vt s"
-and h: "th \<in> set (wq s cs)"
 shows "th \<in> threads s"
 proof -
 from vt and h show ?thesis
 proof(induct arbitrary: th cs)
 case (vt_cons s e)
+interpret vt_s: valid_trace s
+using vt_cons(1) by (unfold_locales, auto)
 assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
 and stp: "step s e"
 and vt: "vt s"
 and h: "th \<in> set (wq (e # s) cs)"
 show ?case
 apply (auto simp:Let_def wq_def split:if_splits)
 proof -
 assume th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
 have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
 proof(rule someI2)
-from wq_distinct[OF vt, of cs'] and eq_wq[folded wq_def]
+from vt_s.wq_distinct[of cs'] and eq_wq[folded wq_def]
 show "distinct rest \<and> set rest = set rest" by auto
 next
 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
 by auto
 qed
 case vt_nil
 thus ?case by (auto simp:wq_def)
 qed
 qed
-lemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
+lemma range_in: "\<lbrakk>(Th th) \<in> Range (RAG (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
 apply(unfold s_RAG_def cs_waiting_def cs_holding_def)
 by (auto intro:wq_threads)
 lemma readys_v_eq:
 fixes th thread cs rest
-assumes vt: "vt s"
+assumes neq_th: "th \<noteq> thread"
-and neq_th: "th \<noteq> thread"
 and eq_wq: "wq s cs = thread#rest"
 and not_in: "th \<notin>  set rest"
 shows "(th \<in> readys (V thread cs#s)) = (th \<in> readys s)"
 proof -
 from assms show ?thesis
 assume th_nin: "th \<notin> set rest"
 and th_in: "th \<in> set (SOME q. distinct q \<and> set q = set rest)"
 and eq_wq: "wq_fun (schs s) cs = thread # rest"
 have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
 proof(rule someI2)
-from wq_distinct[OF vt, of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
+from wq_distinct[of cs, unfolded wq_def] and eq_wq[unfolded wq_def]
 show "distinct rest \<and> set rest = set rest" by auto
 next
 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto
 qed
 with th_nin th_in show False by auto
 by chasing out-going edges, it is always possible to reach a node representing a ready
 thread. In this lemma, it is the @{text "th'"}.
 *}
 lemma chain_building:
-assumes vt: "vt s"
 shows "node \<in> Domain (RAG s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (RAG s)^+)"
 proof -
-from wf_dep_converse [OF vt]
+from wf_dep_converse
 have h: "wf ((RAG s)\<inverse>)" .
 show ?thesis
 proof(induct rule:wf_induct [OF h])
 fix x
 assume ih [rule_format]:
 proof(cases "th' \<in> readys s")
 case True
 from True and th'_d show ?thesis by auto
 next
 case False
-from th'_d and range_in [OF vt] have "th' \<in> threads s" by auto
+from th'_d and range_in  have "th' \<in> threads s" by auto
 with False have "Th th' \<in> Domain (RAG s)"
 by (auto simp:readys_def wq_def s_waiting_def s_RAG_def cs_waiting_def Domain_def)
 from ih [OF th'_d this]
 obtain th'' where
 th''_r: "th'' \<in> readys s" and
 text {* \noindent
 The following is just an instance of @{text "chain_building"}.
 *}
 lemma th_chain_to_ready:
-fixes s th
+assumes th_in: "th \<in> threads s"
-assumes vt: "vt s"
-and th_in: "th \<in> threads s"
 shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
 proof(cases "th \<in> readys s")
 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_def Domain_def)
-from chain_building [rule_format, OF vt this]
+from chain_building [rule_format, OF this]
 show ?thesis by auto
 qed
+end
 lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
 by  (unfold s_waiting_def cs_waiting_def wq_def, auto)
 lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"
 by (unfold s_holding_def wq_def cs_holding_def, simp)
 lemma holding_unique: "\<lbrakk>holding (s::state) th1 cs; holding s th2 cs\<rbrakk> \<Longrightarrow> th1 = th2"
 by (unfold s_holding_def cs_holding_def, auto)
-lemma unique_RAG: "\<lbrakk>vt s; (n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
+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)
 by(auto elim:waiting_unique holding_unique)
+end
 lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
 by (induct rule:trancl_induct, auto)
+context valid_trace
+begin
 lemma dchain_unique:
-assumes vt: "vt s"
+assumes th1_d: "(n, Th th1) \<in> (RAG s)^+"
-and th1_d: "(n, Th th1) \<in> (RAG s)^+"
 and th1_r: "th1 \<in> readys s"
 and th2_d: "(n, Th th2) \<in> (RAG s)^+"
 and th2_r: "th2 \<in> readys s"
 shows "th1 = th2"
 proof -
 { assume neq: "th1 \<noteq> th2"
 hence "Th th1 \<noteq> Th th2" by simp
-from unique_chain [OF _ th1_d th2_d this] and unique_RAG [OF vt]
+from unique_chain [OF _ th1_d th2_d this] and unique_RAG
 have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto
 hence "False"
 proof
 assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+"
 from trancl_split [OF this]
 by (auto simp:readys_def wq_def s_RAG_def s_waiting_def cs_waiting_def)
 with th2_r show ?thesis by auto
 qed
 } thus ?thesis by auto
 qed
+end
 lemma step_holdents_p_add:
 fixes th cs s
 assumes vt: "vt (P th cs#s)"
 from assms show ?thesis
 unfolding  holdents_test step_RAG_p[OF vt] by auto
 qed
-lemma finite_holding:
+lemma (in valid_trace) finite_holding :
-fixes s th cs
-assumes vt: "vt s"
 shows "finite (holdents s th)"
 proof -
 let ?F = "\<lambda> (x, y). the_cs x"
-from finite_RAG [OF vt]
+from finite_RAG
 have "finite (RAG s)" .
 hence "finite (?F `(RAG s))" by simp
 moreover have "{cs . (Cs cs, Th th) \<in> RAG s} \<subseteq> \<dots>"
 proof -
 { have h: "\<And> a A f. a \<in> A \<Longrightarrow> f a \<in> f ` A" by auto
 lemma cntCS_v_dec:
 fixes s thread cs
 assumes vtv: "vt (V thread cs#s)"
 shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
 proof -
+from vtv interpret vt_s: valid_trace s
+by (cases, unfold_locales, simp)
+from vtv interpret vt_v: valid_trace "V thread cs#s"
+by (unfold_locales, simp)
 from step_back_step[OF vtv]
 have cs_in: "cs \<in> holdents s thread"
 apply (cases, unfold holdents_test s_RAG_def, simp)
 by (unfold cs_holding_def s_holding_def wq_def, auto)
 moreover have cs_not_in:
 "(holdents (V thread cs#s) thread) = holdents s thread - {cs}"
-apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs])
+apply (insert vt_s.wq_distinct[of cs])
 apply (unfold holdents_test, unfold step_RAG_v[OF vtv],
 auto simp:next_th_def)
 proof -
 fix rest
 assume dst: "distinct (rest::thread list)"
 have "holdents s thread = insert cs (holdents (V thread cs#s) thread)"
 by auto
 moreover have "card \<dots> =
 Suc (card ((holdents (V thread cs#s) thread) - {cs}))"
 proof(rule card_insert)
-from finite_holding [OF vtv]
+from vt_v.finite_holding
 show " finite (holdents (V thread cs # s) thread)" .
 qed
 moreover from cs_not_in
 have "cs \<notin> (holdents (V thread cs#s) thread)" by auto
 ultimately show ?thesis by (simp add:cntCS_def)
 qed
+context valid_trace
+begin
 text {* (* ddd *) \noindent
 The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"}
 of one particular thread.
 *}
 lemma cnp_cnv_cncs:
-fixes s th
-assumes vt: "vt s"
 shows "cntP s th = cntV s th + (if (th \<in> readys s \<or> th \<notin> threads s)
 then cntCS s th else cntCS s th + 1)"
 proof -
 from vt show ?thesis
 proof(induct arbitrary:th)
 case (vt_cons s e)
+interpret vt_s: valid_trace s using vt_cons(1) by (unfold_locales, simp)
 assume vt: "vt s"
 and ih: "\<And>th. cntP s th  = cntV s th +
 (if (th \<in> readys s \<or> th \<notin> threads s) then cntCS s th else cntCS s th + 1)"
 and stp: "step s e"
 from stp show ?case
 and not_in: "thread \<notin> threads s"
 show ?thesis
 proof -
 { fix cs
 assume "thread \<in> set (wq s cs)"
-from wq_threads [OF vt this] have "thread \<in> threads s" .
+from vt_s.wq_threads [OF this] have "thread \<in> threads s" .
 with not_in have "False" by simp
 } with eq_e have eq_readys: "readys (e#s) = readys s \<union> {thread}"
 by (auto simp:readys_def threads.simps s_waiting_def
 wq_def cs_waiting_def Let_def)
 from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def)
 case (thread_P thread cs)
 assume eq_e: "e = P thread cs"
 and is_runing: "thread \<in> runing s"
 and no_dep: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"
 from thread_P vt stp ih  have vtp: "vt (P thread cs#s)" by auto
+then interpret vt_p: valid_trace "(P thread cs#s)"
+by (unfold_locales, simp)
 show ?thesis
 proof -
 { have hh: "\<And> A B C. (B = C) \<Longrightarrow> (A \<and> B) = (A \<and> C)" by blast
 assume neq_th: "th \<noteq> thread"
 with eq_e
 Suc (card {cs. (Cs cs, Th thread) \<in> RAG s})" (is "card ?L = Suc (card ?R)")
 proof -
 have "?L = insert cs ?R" by auto
 moreover have "card \<dots> = Suc (card (?R - {cs}))"
 proof(rule card_insert)
-from finite_holding [OF vt, of thread]
+from vt_s.finite_holding [of thread]
 show " finite {cs. (Cs cs, Th thread) \<in> RAG s}"
 by (unfold holdents_test, simp)
 qed
 moreover have "?R - {cs} = ?R"
 proof -
 by (simp add:s_waiting_def wq_def)
 moreover from eq_wq have "th \<in> set (wq (e#s) cs)" by auto
 ultimately have "th = hd (wq (e#s) cs)" by blast
 with eq_wq have "th = hd (wq s cs @ [th])" by simp
 hence "th = hd (wq s cs)" using False by auto
-with False eq_wq wq_distinct [OF vtp, of cs]
+with False eq_wq vt_p.wq_distinct [of cs]
 show False by (fold eq_e, auto)
 qed
 moreover from is_runing have "th \<in> threads (e#s)"
 by (unfold eq_e, auto simp:runing_def readys_def eq_th)
 moreover have "cntCS (e # s) th = cntCS s th"
 } ultimately show ?thesis by blast
 qed
 next
 case (thread_V thread cs)
 from assms vt stp ih thread_V have vtv: "vt (V thread cs # s)" by auto
+then interpret vt_v: valid_trace "(V thread cs # s)" by (unfold_locales, simp)
 assume eq_e: "e = V thread cs"
 and is_runing: "thread \<in> runing s"
 and hold: "holding s thread cs"
 from hold obtain rest
 where eq_wq: "wq s cs = thread # rest"
 by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
 have eq_threads: "threads (e#s) = threads s" by (simp add: eq_e)
 have eq_set: "set (SOME q. distinct q \<and> set q = set rest) = set rest"
 proof(rule someI2)
-from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
+from vt_v.wq_distinct[of cs] and eq_wq
-show "distinct rest \<and> set rest = set rest" by auto
+show "distinct rest \<and> set rest = set rest"
+by (metis distinct.simps(2) vt_s.wq_distinct)
 next
 show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
 by auto
 qed
 show ?thesis
 apply(unfold eq_e wq_def eq_cs s_holding_def)
 apply (auto simp:Let_def)
 proof -
 assume "thread \<in> set (SOME q. distinct q \<and> set q = set rest)"
 with eq_set have "thread \<in> set rest" by simp
-with wq_distinct[OF step_back_vt[OF vtv], of cs]
+with vt_v.wq_distinct[of cs]
-and eq_wq show False by auto
+and eq_wq show False
+by (metis distinct.simps(2) vt_s.wq_distinct)
 qed
 thus ?thesis by (simp add:wq_def s_waiting_def)
 qed
 } moreover {
 assume neq_cs: "cs1 \<noteq> cs"
 have ?thesis
 proof(cases "th \<in> set rest")
 case False
 have "(th \<in> readys (e # s)) = (th \<in> readys s)"
 apply (insert step_back_vt[OF vtv])
-by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto)
+by (simp add: False eq_e eq_wq neq_th vt_s.readys_v_eq)
 moreover have "cntCS (e#s) th = cntCS s th"
 apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
 proof -
 have "{csa. (Cs csa, Th th) \<in> RAG s \<or> csa = cs \<and> next_th s thread cs th} =
 {cs. (Cs cs, Th th) \<in> RAG s}"
 from eq_set ni have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>
 set (SOME q. distinct q \<and> set q = set rest)
 " by simp
 moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 proof(rule someI2)
-from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
+from vt_s.wq_distinct[ of cs] and eq_wq
 show "distinct rest \<and> set rest = set rest" by auto
 next
 fix x assume "distinct x \<and> set x = set rest"
 with ne show "x \<noteq> []" by auto
 qed
 proof -
 from eq_wq and th_in
 have "\<not> th \<in> readys s"
 apply (auto simp:readys_def s_waiting_def)
 apply (rule_tac x = cs in exI, auto)
-by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp add: wq_def)
+by (insert vt_s.wq_distinct[of cs], auto simp add: wq_def)
 moreover
 from eq_wq and th_in and neq_hd
 have "\<not> (th \<in> readys (e # s))"
 apply (auto simp:readys_def s_waiting_def eq_e wq_def Let_def split:list.splits)
 by (rule_tac x = cs in exI, auto simp:eq_set)
 from eq_wq and  th_in and neq_hd
 have "(holdents (e # s) th) = (holdents s th)"
 apply (unfold eq_e step_RAG_v[OF vtv],
 auto simp:next_th_def eq_set s_RAG_def holdents_test wq_def
 Let_def cs_holding_def)
-by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def)
+by (insert vt_s.wq_distinct[of cs], auto simp:wq_def)
 thus ?thesis by (simp add:cntCS_def)
 qed
 moreover note ih eq_cnp eq_cnv eq_threads
 ultimately show ?thesis by auto
 next
 Let_def next_th_def)
 proof -
 assume eq_wq: "wq_fun (schs s) cs = thread # rest"
 and t_in: "?t \<in> set rest"
 show "?t \<in> threads s"
-proof(rule wq_threads[OF step_back_vt[OF vtv]])
+proof(rule vt_s.wq_threads)
 from eq_wq and t_in
 show "?t \<in> set (wq s cs)" by (auto simp:wq_def)
 qed
 next
 fix csa
 and neq_cs: "csa \<noteq> cs"
 and t_in': "?t \<in>  set (wq_fun (schs s) csa)"
 show "?t = hd (wq_fun (schs s) csa)"
 proof -
 { assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)"
-from wq_distinct[OF step_back_vt[OF vtv], of cs] and
+from vt_s.wq_distinct[of cs] and
 eq_wq[folded wq_def] and t_in eq_wq
 have "?t \<noteq> thread" by auto
 with eq_wq and t_in
 have w1: "waiting s ?t cs"
 by (auto simp:s_waiting_def wq_def)
 from t_in' neq_hd'
 have w2: "waiting s ?t csa"
 by (auto simp:s_waiting_def wq_def)
-from waiting_unique[OF step_back_vt[OF vtv] w1 w2]
+from vt_s.waiting_unique[OF w1 w2]
 and neq_cs have "False" by auto
 } thus ?thesis by auto
 qed
 qed
 moreover have "cntP s th = cntV s th + cntCS s th + 1"
 qed
 moreover have "th \<in> threads s"
 proof -
 from th_in eq_wq
 have "th \<in> set (wq s cs)" by simp
-from wq_threads [OF step_back_vt[OF vtv] this]
+from vt_s.wq_threads [OF this]
 show ?thesis .
 qed
 ultimately show ?thesis using ih by auto
 qed
 moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th"
 also have "\<dots> = Suc (card ?B)"
 proof(rule card_insert_disjoint)
 have "?B \<subseteq> ((\<lambda> (x, y). the_cs x) ` RAG s)"
 apply (auto simp:image_def)
 by (rule_tac x = "(Cs x, Th th)" in bexI, auto)
-with finite_RAG[OF step_back_vt[OF vtv]]
+with vt_s.finite_RAG
 show "finite {cs. (Cs cs, Th th) \<in> RAG s}" by (auto intro:finite_subset)
 next
 show "cs \<notin> {cs. (Cs cs, Th th) \<in> RAG s}"
 proof
 assume "cs \<in> {cs. (Cs cs, Th th) \<in> RAG s}"
 auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
 qed
 qed
 lemma not_thread_cncs:
-fixes th s
+assumes not_in: "th \<notin> threads s"
-assumes vt: "vt s"
-and not_in: "th \<notin> threads s"
 shows "cntCS s th = 0"
 proof -
 from vt not_in show ?thesis
 proof(induct arbitrary:th)
 case (vt_cons s e th)
+interpret vt_s: valid_trace s using vt_cons(1)
+by (unfold_locales, simp)
 assume vt: "vt s"
 and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> cntCS s th = 0"
 and stp: "step s e"
 and not_in: "th \<notin> threads (e # s)"
 from stp show ?case
 from not_in eq_e have "th \<notin> threads s" by simp
 moreover from is_runing have "thread \<in> threads s"
 by (simp add:runing_def readys_def)
 ultimately show ?thesis by auto
 qed
-from assms thread_V vt stp ih have vtv: "vt (V thread cs#s)" by auto
+from assms thread_V vt stp ih
+have vtv: "vt (V thread cs#s)" by auto
+then interpret vt_v: valid_trace "(V thread cs#s)"
+by (unfold_locales, simp)
 from hold obtain rest
 where eq_wq: "wq s cs = thread # rest"
 by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
 from not_in eq_e eq_wq
 have "\<not> next_th s thread cs th"
 proof -
 assume ne: "rest \<noteq> []"
 and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")
 have "?t \<in> set rest"
 proof(rule someI2)
-from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq
+from vt_v.wq_distinct[of cs] and eq_wq
-show "distinct rest \<and> set rest = set rest" by auto
+show "distinct rest \<and> set rest = set rest"
+by (metis distinct.simps(2) vt_s.wq_distinct)
 next
 fix x assume "distinct x \<and> set x = set rest" with ne
 show "hd x \<in> set rest" by (cases x, auto)
 qed
 with eq_wq have "?t \<in> set (wq s cs)" by simp
-from wq_threads[OF step_back_vt[OF vtv], OF this] and ni
+from vt_s.wq_threads[OF this] and ni
-show False by auto
+show False
+using `hd (SOME q. distinct q \<and> set q = set rest) \<in> set (wq s cs)`
+ni vt_s.wq_threads by blast
 qed
 moreover note neq_th eq_wq
 ultimately have "cntCS (e # s) th  = cntCS s th"
 by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)
 moreover have "cntCS s th = 0"
 by (unfold cntCS_def,
 auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)
 qed
 qed
+end
 lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
 by (auto simp:s_waiting_def cs_waiting_def wq_def)
+context valid_trace
+begin
 lemma dm_RAG_threads:
-fixes th s
+assumes in_dom: "(Th th) \<in> Domain (RAG s)"
-assumes vt: "vt s"
-and in_dom: "(Th th) \<in> Domain (RAG s)"
 shows "th \<in> threads s"
 proof -
 from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
 moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by 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_def)
-from wq_threads [OF vt this] show ?thesis .
+from wq_threads [OF this] show ?thesis .
 qed
+end
 lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"
 unfolding cp_def wq_def
 apply(induct s rule: schs.induct)
 thm cpreced_initial
 apply(simp add: Let_def)
 apply(subst (2) schs.simps)
 apply(simp add: Let_def)
 done
-(* FIXME: NOT NEEDED *)
+context valid_trace
+begin
 lemma runing_unique:
-fixes th1 th2 s
+assumes runing_1: "th1 \<in> runing s"
-assumes vt: "vt s"
-and runing_1: "th1 \<in> runing s"
 and runing_2: "th2 \<in> runing s"
 shows "th1 = th2"
 proof -
 from runing_1 and runing_2 have "cp s th1 = cp s th2"
 unfolding runing_def
 have "{th'. (Th th', Th th1) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)"
 apply (auto simp:image_def)
 by (rule_tac x = "(Th x, Th th1)" in bexI, auto)
 moreover have "finite \<dots>"
 proof -
-from finite_RAG[OF vt] have "finite (RAG s)" .
+from finite_RAG have "finite (RAG s)" .
 hence "finite ((RAG (wq s))\<^sup>+)"
 apply (unfold finite_trancl)
 by (auto simp: s_RAG_def cs_RAG_def wq_def)
 thus ?thesis by auto
 qed
 have "{th'. (Th th', Th th2) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)"
 apply (auto simp:image_def)
 by (rule_tac x = "(Th x, Th th2)" in bexI, auto)
 moreover have "finite \<dots>"
 proof -
-from finite_RAG[OF vt] have "finite (RAG s)" .
+from finite_RAG have "finite (RAG s)" .
 hence "finite ((RAG (wq s))\<^sup>+)"
 apply (unfold finite_trancl)
 by (auto simp: s_RAG_def cs_RAG_def wq_def)
 thus ?thesis by auto
 qed
 assume "th1' \<in> dependants (wq s) th1"
 hence "(Th th1') \<in> Domain ((RAG s)^+)"
 apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
 by (auto simp:Domain_def)
 hence "(Th th1') \<in> Domain (RAG s)" by (simp add:trancl_domain)
-from dm_RAG_threads[OF vt this] show ?thesis .
+from dm_RAG_threads[OF this] show ?thesis .
 next
 assume "th1' = th1"
 with runing_1 show ?thesis
 by (unfold runing_def readys_def, auto)
 qed
 assume "th2' \<in> dependants (wq s) th2"
 hence "(Th th2') \<in> Domain ((RAG s)^+)"
 apply (unfold cs_dependants_def cs_RAG_def s_RAG_def)
 by (auto simp:Domain_def)
 hence "(Th th2') \<in> Domain (RAG s)" by (simp add:trancl_domain)
-from dm_RAG_threads[OF vt this] show ?thesis .
+from dm_RAG_threads[OF this] show ?thesis .
 next
 assume "th2' = th2"
 with runing_2 show ?thesis
 by (unfold runing_def readys_def, auto)
 qed
 hence h1: "(Th th1', Th th2) \<in> (RAG s)^+"
 by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
 from th1'_in have h2: "(Th th1', Th th1) \<in> (RAG s)^+"
 by (unfold cs_dependants_def s_RAG_def cs_RAG_def, simp)
 show ?thesis
-proof(rule dchain_unique[OF vt h1 _ h2, symmetric])
+proof(rule dchain_unique[OF h1 _ h2, symmetric])
 from runing_1 show "th1 \<in> readys s" by (simp add:runing_def)
 from runing_2 show "th2 \<in> readys s" by (simp add:runing_def)
 qed
 qed
 qed
 qed
-lemma "vt s \<Longrightarrow> card (runing s) \<le> 1"
+lemma "card (runing s) \<le> 1"
 apply(subgoal_tac "finite (runing s)")
 prefer 2
 apply (metis finite_nat_set_iff_bounded lessI runing_unique)
 apply(rule ccontr)
 apply(simp)
 apply(auto)[1]
 apply (metis insertCI runing_unique)
 apply(auto)
 done
+end
 lemma create_pre:
 assumes stp: "step s e"
 and not_in: "th \<notin> threads s"
 and is_in: "th \<in> threads (e#s)"
 obtains prio where "e = Create th prio"
 ultimately have eq_me: "moment (Suc i) t = e#(moment i t)"
 by (auto simp:down_to_moment)
 from that [OF this] show ?thesis .
 qed
+context valid_trace
+begin
 lemma cnp_cnv_eq:
-fixes th s
+assumes "th \<notin> threads s"
-assumes "vt s"
-and "th \<notin> threads s"
 shows "cntP s th = cntV s th"
-by (simp add: assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
+using assms
+using cnp_cnv_cncs not_thread_cncs by auto
+end
 lemma eq_RAG:
 "RAG (wq s) = RAG s"
 by (unfold cs_RAG_def s_RAG_def, auto)
+context valid_trace
+begin
 lemma count_eq_dependants:
-assumes vt: "vt s"
+assumes eq_pv: "cntP s th = cntV s th"
-and eq_pv: "cntP s th = cntV s th"
 shows "dependants (wq s) th = {}"
 proof -
-from cnp_cnv_cncs[OF vt] and eq_pv
+from cnp_cnv_cncs and eq_pv
 have "cntCS s th = 0"
 by (auto split:if_splits)
 moreover have "finite {cs. (Cs cs, Th th) \<in> RAG s}"
 proof -
-from finite_holding[OF vt, of th] show ?thesis
+from finite_holding[of th] show ?thesis
 by (simp add:holdents_test)
 qed
 ultimately have h: "{cs. (Cs cs, Th th) \<in> RAG s} = {}"
 by (unfold cntCS_def holdents_test cs_dependants_def, auto)
 show ?thesis
 } thus "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} = {}" by auto
 qed
 qed
 lemma dependants_threads:
-fixes s th
-assumes vt: "vt s"
 shows "dependants (wq s) th \<subseteq> threads s"
 proof
 { fix th th'
 assume h: "th \<in> {th'a. (Th th'a, Th th') \<in> (RAG (wq s))\<^sup>+}"
 have "Th th \<in> Domain (RAG s)"
 from h obtain th' where "(Th th, Th th') \<in> (RAG (wq s))\<^sup>+" by auto
 hence "(Th th) \<in> Domain ( (RAG (wq s))\<^sup>+)" by (auto simp:Domain_def)
 with trancl_domain have "(Th th) \<in> Domain (RAG (wq s))" by simp
 thus ?thesis using eq_RAG by simp
 qed
-from dm_RAG_threads[OF vt this]
+from dm_RAG_threads[OF this]
 have "th \<in> threads s" .
 } note hh = this
 fix th1
 assume "th1 \<in> dependants (wq s) th"
 hence "th1 \<in> {th'a. (Th th'a, Th th) \<in> (RAG (wq s))\<^sup>+}"
 by (unfold cs_dependants_def, simp)
 from hh [OF this] show "th1 \<in> threads s" .
 qed
 lemma finite_threads:
-assumes vt: "vt s"
 shows "finite (threads s)"
-using vt
+using vt by (induct) (auto elim: step.cases)
-by (induct) (auto elim: step.cases)
+end
 lemma Max_f_mono:
 assumes seq: "A \<subseteq> B"
 and np: "A \<noteq> {}"
 and fnt: "finite B"
 from np show "f ` A \<noteq> {}" by auto
 next
 from fnt and seq show "finite (f ` B)" by auto
 qed
+context valid_trace
+begin
 lemma cp_le:
-assumes vt: "vt s"
+assumes th_in: "th \<in> threads s"
-and th_in: "th \<in> threads s"
 shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
 proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
 show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))
 \<le> Max ((\<lambda>th. preced th s) ` threads s)"
 (is "Max (?f ` ?A) \<le> Max (?f ` ?B)")
 proof(rule Max_f_mono)
 show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp
 next
-from finite_threads [OF vt]
+from finite_threads
 show "finite (threads s)" .
 next
 from th_in
 show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"
 apply (auto simp:Domain_def)
-apply (rule_tac dm_RAG_threads[OF vt])
+apply (rule_tac dm_RAG_threads)
 apply (unfold trancl_domain [of "RAG s", symmetric])
 by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)
 qed
 qed
 lemma le_cp:
-assumes vt: "vt s"
 shows "preced th s \<le> cp s th"
 proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
 show "Prc (priority th s) (last_set th s)
 \<le> Max (insert (Prc (priority th s) (last_set th s))
 ((\<lambda>th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))"
 have "{th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> ?F ` ((RAG (wq s))\<^sup>+)"
 apply (auto simp:image_def)
 by (rule_tac x = "(Th x, Th th)" in bexI, auto)
 moreover have "finite \<dots>"
 proof -
-from finite_RAG[OF vt] have "finite (RAG s)" .
+from finite_RAG have "finite (RAG s)" .
 hence "finite ((RAG (wq s))\<^sup>+)"
 apply (unfold finite_trancl)
 by (auto simp: s_RAG_def cs_RAG_def wq_def)
 thus ?thesis by auto
 qed
 thus ?thesis by auto
 qed
 qed
 lemma max_cp_eq:
-assumes vt: "vt s"
 shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
 (is "?l = ?r")
 proof(cases "threads s = {}")
 case True
 thus ?thesis by auto
 next
 case False
 have "?l \<in> ((cp s) ` threads s)"
 proof(rule Max_in)
-from finite_threads[OF vt]
+from finite_threads
 show "finite (cp s ` threads s)" by auto
 next
 from False show "cp s ` threads s \<noteq> {}" by auto
 qed
 then obtain th
 where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto
-have "\<dots> \<le> ?r" by (rule cp_le[OF vt th_in])
+have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])
 moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")
 proof -
 have "?r \<in> (?f ` ?A)"
 proof(rule Max_in)
-from finite_threads[OF vt]
+from finite_threads
 show " finite ((\<lambda>th. preced th s) ` threads s)" by auto
 next
 from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto
 qed
 then obtain th' where
 th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto
-from le_cp [OF vt, of th']  eq_r
+from le_cp [of th']  eq_r
 have "?r \<le> cp s th'" by auto
 moreover have "\<dots> \<le> cp s th"
 proof(fold eq_l)
 show " cp s th' \<le> Max (cp s ` threads s)"
 proof(rule Max_ge)
 from th_in' show "cp s th' \<in> cp s ` threads s"
 by auto
 next
-from finite_threads[OF vt]
+from finite_threads
 show "finite (cp s ` threads s)" by auto
 qed
 qed
 ultimately show ?thesis by auto
 qed
 ultimately show ?thesis using eq_l by auto
 qed
 lemma max_cp_readys_threads_pre:
-assumes vt: "vt s"
+assumes np: "threads s \<noteq> {}"
-and np: "threads s \<noteq> {}"
 shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
-proof(unfold max_cp_eq[OF vt])
+proof(unfold max_cp_eq)
 show "Max (cp s ` readys s) = Max ((\<lambda>th. preced th s) ` threads s)"
 proof -
 let ?p = "Max ((\<lambda>th. preced th s) ` threads s)"
 let ?f = "(\<lambda>th. preced th s)"
 have "?p \<in> ((\<lambda>th. preced th s) ` threads s)"
 proof(rule Max_in)
-from finite_threads[OF vt] show "finite (?f ` threads s)" by simp
+from finite_threads show "finite (?f ` threads s)" by simp
 next
 from np show "?f ` threads s \<noteq> {}" by simp
 qed
 then obtain tm where tm_max: "?f tm = ?p" and tm_in: "tm \<in> threads s"
 by (auto simp:Image_def)
-from th_chain_to_ready [OF vt tm_in]
+from th_chain_to_ready [OF tm_in]
 have "tm \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+)" .
 thus ?thesis
 proof
 assume "\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (RAG s)\<^sup>+ "
 then obtain th' where th'_in: "th' \<in> readys s"
 and tm_chain:"(Th tm, Th th') \<in> (RAG s)\<^sup>+" by auto
 have "cp s th' = ?f tm"
 proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
-from dependants_threads[OF vt] finite_threads[OF vt]
+from dependants_threads finite_threads
 show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))"
 by (auto intro:finite_subset)
 next
 fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"
 from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .
 moreover have "p \<le> \<dots>"
 proof(rule Max_ge)
-from finite_threads[OF vt]
+from finite_threads
 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
 next
-from p_in and th'_in and dependants_threads[OF vt, of th']
+from p_in and th'_in and dependants_threads[of th']
 show "p \<in> (\<lambda>th. preced th s) ` threads s"
 by (auto simp:readys_def)
 qed
 ultimately show "p \<le> preced tm s" by auto
 next
 show "q \<le> cp s th'"
 apply (unfold h eq_q)
 apply (unfold cp_eq_cpreced cpreced_def)
 apply (rule Max_mono)
 proof -
-from dependants_threads [OF vt, of th1] th1_in
+from dependants_threads [of th1] th1_in
 show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq>
 (\<lambda>th. preced th s) ` threads s"
 by (auto simp:readys_def)
 next
 show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp
 next
-from finite_threads[OF vt]
+from finite_threads
 show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
 qed
 next
-from finite_threads[OF vt]
+from finite_threads
 show "finite (cp s ` readys s)" by (auto simp:readys_def)
 next
 from th'_in
 show "cp s th' \<in> cp s ` readys s" by simp
 qed
 proof -
 { fix y'
 assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"
 have "y' \<le> preced tm s"
 proof(unfold tm_max, rule Max_ge)
-from hy' dependants_threads[OF vt, of tm]
+from hy' dependants_threads[of tm]
 show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
 next
-from finite_threads[OF vt]
+from finite_threads
 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
 qed
 } with hy show ?thesis by auto
 qed
 next
-from dependants_threads[OF vt, of tm] finite_threads[OF vt]
+from dependants_threads[of tm] finite_threads
 show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"
 by (auto intro:finite_subset)
 next
 show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"
 by simp
 qed
 moreover have "Max (cp s ` readys s) = cp s tm"
 proof(rule Max_eqI)
 from tm_ready show "cp s tm \<in> cp s ` readys s" by simp
 next
-from finite_threads[OF vt]
+from finite_threads
 show "finite (cp s ` readys s)" by (auto simp:readys_def)
 next
 fix y assume "y \<in> cp s ` readys s"
 then obtain th1 where th1_readys: "th1 \<in> readys s"
 and h: "y = cp s th1" by auto
 show "y \<le> cp s tm"
 apply(unfold cp_eq_p h)
 apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono)
 proof -
-from finite_threads[OF vt]
+from finite_threads
 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
 next
 show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"
 by simp
 next
-from dependants_threads[OF vt, of th1] th1_readys
+from dependants_threads[of th1] th1_readys
 show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)
 \<subseteq> (\<lambda>th. preced th s) ` threads s"
 by (auto simp:readys_def)
 qed
 qed
 text {* (* ccc *) \noindent
 Since the current precedence of the threads in ready queue will always be boosted,
 there must be one inside it has the maximum precedence of the whole system.
 *}
 lemma max_cp_readys_threads:
-assumes vt: "vt s"
 shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
 proof(cases "threads s = {}")
 case True
 thus ?thesis
 by (auto simp:readys_def)
 next
 case False
-show ?thesis by (rule max_cp_readys_threads_pre[OF vt False])
+show ?thesis by (rule max_cp_readys_threads_pre[OF False])
 qed
+end
 lemma eq_holding: "holding (wq s) th cs = holding s th cs"
 apply (unfold s_holding_def cs_holding_def wq_def, simp)
 done
 apply(simp add: Domain_iff Range_iff)
 apply(simp add: wq_def)
 apply(auto)
 done
+context valid_trace
+begin
 lemma detached_intro:
-fixes s th
+assumes eq_pv: "cntP s th = cntV s th"
-assumes vt: "vt s"
-and eq_pv: "cntP s th = cntV s th"
 shows "detached s th"
 proof -
-from cnp_cnv_cncs[OF vt]
+from cnp_cnv_cncs
 have eq_cnt: "cntP s th =
 cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
 hence cncs_zero: "cntCS s th = 0"
 by (auto simp:eq_pv split:if_splits)
 with eq_cnt
 have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:eq_pv)
 thus ?thesis
 proof
 assume "th \<notin> threads s"
-with range_in[OF vt] dm_RAG_threads[OF vt]
+with range_in dm_RAG_threads
 show ?thesis
 by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff)
 next
 assume "th \<in> readys s"
 moreover have "Th th \<notin> Range (RAG s)"
 proof -
-from card_0_eq [OF finite_holding [OF vt]] and cncs_zero
+from card_0_eq [OF finite_holding] and cncs_zero
 have "holdents s th = {}"
 by (simp add:cntCS_def)
 thus ?thesis
 apply(auto simp:holdents_test)
 apply(case_tac a)
 by (auto simp add: detached_def s_RAG_def s_waiting_abv s_holding_abv wq_def readys_def)
 qed
 qed
 lemma detached_elim:
-fixes s th
+assumes dtc: "detached s th"
-assumes vt: "vt s"
-and dtc: "detached s th"
 shows "cntP s th = cntV s th"
 proof -
-from cnp_cnv_cncs[OF vt]
+from cnp_cnv_cncs
 have eq_pv: " cntP s th =
 cntV s th + (if th \<in> readys s \<or> th \<notin> threads s then cntCS s th else cntCS s th + 1)" .
 have cncs_z: "cntCS s th = 0"
 proof -
 from dtc have "holdents s th = {}"
 with cncs_z and eq_pv show ?thesis by simp
 qed
 qed
 lemma detached_eq:
-fixes s th
-assumes vt: "vt s"
 shows "(detached s th) = (cntP s th = cntV s th)"
 by (insert vt, auto intro:detached_intro detached_elim)
+end
 text {*
 The lemmas in this .thy file are all obvious lemmas, however, they still needs to be derived
 from the concise and miniature model of PIP given in PrioGDef.thy.
 *}
 assumes nt1: "next_th s th cs th1"
 and nt2: "next_th s th cs th2"
 shows "th1 = th2"
 using assms by (unfold next_th_def, auto)
+lemma birth_time_lt:  "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
+apply (induct s, simp)
+proof -
+fix a s
+assume ih: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
+and eq_as: "a # s \<noteq> []"
+show "last_set th (a # s) < length (a # s)"
+proof(cases "s \<noteq> []")
+case False
+from False show ?thesis
+by (cases a, auto simp:last_set.simps)
+next
+case True
+from ih [OF True] show ?thesis
+by (cases a, auto simp:last_set.simps)
+qed
+qed
+lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
+by (induct s, auto simp:threads.simps)
+lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
+apply (drule_tac th_in_ne)
+by (unfold preced_def, auto intro: birth_time_lt)
 end

changeset 63	b620a2a0806a
parent 62	031d2ae9c9b8