regexp: comparison prio/PrioG.thy

equal deleted inserted replaced

-:0a4be67ea7f8
+:f2e0d031a395
 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 step s \<Longrightarrow> distinct (wq s cs)"
+lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"
 proof(erule_tac vt.induct, simp add:wq_def)
 fix s e
 assume h1: "step s e"
 and h2: "distinct (wq s cs)"
 thus "distinct (wq (e # s) cs)"
 thus "distinct q" by auto
 qed
 qed
 qed
-lemma step_back_vt: "vt ccs (e#s) \<Longrightarrow> vt ccs s"
+lemma step_back_vt: "vt (e#s) \<Longrightarrow> vt s"
-by(ind_cases "vt ccs (e#s)", simp)
+by(ind_cases "vt (e#s)", simp)
-lemma step_back_step: "vt ccs (e#s) \<Longrightarrow> ccs s e"
+lemma step_back_step: "vt (e#s) \<Longrightarrow> step s e"
-by(ind_cases "vt ccs (e#s)", simp)
+by(ind_cases "vt (e#s)", simp)
 lemma block_pre:
 fixes thread cs s
-assumes vt_e: "vt step (e#s)"
+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 -
 fix q qs
 assume h1: "thread \<notin> set (wq_fun (schs s) cs)"
 and h2: "q # qs = wq_fun (schs s) cs"
 and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
-and vt: "vt step (V th cs # s)"
+and vt: "vt (V th cs # s)"
 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)
 ultimately show "False" by auto
 qed
 qed
 qed
-lemma p_pre: "\<lbrakk>vt step ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
+lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow>
 thread \<in> runing s \<and> (Cs cs, Th thread)  \<notin> (depend s)^+"
-apply (ind_cases "vt step ((P thread cs)#s)")
+apply (ind_cases "vt ((P thread cs)#s)")
 apply (ind_cases "step s (P thread cs)")
 by auto
 lemma abs1:
 fixes e es
 qed
 lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"
 by (cases es, auto)
-inductive_cases evt_cons: "vt cs (a#s)"
+inductive_cases evt_cons: "vt (a#s)"
 lemma abs2:
-assumes vt: "vt step (e#s)"
+assumes vt: "vt (e#s)"
 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"
 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 -
 fix th qs
-assume vt: "vt step (V th cs # s)"
+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]
 ultimately show ?thesis by auto
 qed
 qed
 qed
-lemma vt_moment: "\<And> t. \<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
+lemma vt_moment: "\<And> t. \<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
 proof(induct s, simp)
 fix a s t
-assume h: "\<And>t.\<lbrakk>vt cs s; t \<le> length s\<rbrakk> \<Longrightarrow> vt cs (moment t s)"
+assume h: "\<And>t.\<lbrakk>vt s; t \<le> length s\<rbrakk> \<Longrightarrow> vt (moment t s)"
-and vt_a: "vt cs (a # s)"
+and vt_a: "vt (a # s)"
 and le_t: "t \<le> length (a # s)"
-show "vt cs (moment t (a # s))"
+show "vt (moment t (a # s))"
 proof(cases "t = length (a#s)")
 case True
 from True have "moment t (a#s) = a#s" by simp
 with vt_a show ?thesis by simp
 next
 case False
 with le_t have le_t1: "t \<le> length s" by simp
-from vt_a have "vt cs s"
+from vt_a have "vt s"
 by (erule_tac evt_cons, simp)
-from h [OF this le_t1] have "vt cs (moment t s)" .
+from h [OF this le_t1] have "vt (moment t s)" .
 moreover have "moment t (a#s) = moment t s"
 proof -
 from moment_app [OF le_t1, of "[a]"]
 show ?thesis by simp
 qed
 lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
 *)
 lemma waiting_unique_pre:
 fixes cs1 cs2 s thread
-assumes vt: "vt step s"
+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"
 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 step (e#moment t2 s)"
+have vt_e: "vt (e#moment t2 s)"
 proof -
 from vt_moment [OF vt le_t3]
-have "vt step (moment ?t3 s)" .
+have "vt (moment ?t3 s)" .
 with eq_m show ?thesis by simp
 qed
 have ?thesis
 proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
 case True
 show ?thesis by auto
 next
 case False
 from block_pre [OF vt_e False h1]
 have "e = P thread cs2" .
-with vt_e have "vt step ((P thread cs2)# moment t2 s)" by simp
+with 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 s_waiting_def, auto)
+show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)
 qed
 } moreover {
 assume lt12: "t2 < t1"
 let ?t3 = "Suc t1"
 from lt1 have le_t3: "?t3 \<le> length s" by auto
 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 step (e#moment t1 s)"
+have vt_e: "vt  (e#moment t1 s)"
 proof -
 from vt_moment [OF vt le_t3]
-have "vt step (moment ?t3 s)" .
+have "vt (moment ?t3 s)" .
 with eq_m show ?thesis by simp
 qed
 have ?thesis
 proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
 case True
 show ?thesis by auto
 next
 case False
 from block_pre [OF vt_e False h1]
 have "e = P thread cs1" .
-with vt_e have "vt step ((P thread cs1)# moment t1 s)" by simp
+with 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 s_waiting_def, auto)
+show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)
 qed
 } moreover {
 assume eqt12: "t1 = t2"
 let ?t3 = "Suc t1"
 from lt1 have le_t3: "?t3 \<le> length s" by auto
 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 step (e#moment t1 s)"
+have vt_e: "vt (e#moment t1 s)"
 proof -
 from vt_moment [OF vt le_t3]
-have "vt step (moment ?t3 s)" .
+have "vt (moment ?t3 s)" .
 with eq_m show ?thesis by simp
 qed
 have ?thesis
 proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
 case True
 show ?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
-from vt_e and eqt12 have "vt step (e#moment t2 s)" by simp
+from vt_e and eqt12 have "vt (e#moment t2 s)" by simp
 from abs2 [OF this True eq_th h2 h1]
 show ?thesis .
 next
 case False
-have vt_e: "vt step (e#moment t2 s)"
+have vt_e: "vt (e#moment t2 s)"
 proof -
 from vt_moment [OF vt le_t3] eqt12
-have "vt step (moment (Suc t2) s)" by auto
+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]
 have "e = P thread cs2" .
 with eq_e1 neq12 show ?thesis by auto
 qed
 qed
 lemma waiting_unique:
 fixes s cs1 cs2
-assumes "vt step s"
+assumes "vt s"
 and "waiting s th cs1"
 and "waiting s th cs2"
 shows "cs1 = cs2"
 proof -
 from waiting_unique_pre and prems
 show ?thesis
-by (auto simp add:s_waiting_def)
+by (auto simp add: wq_def s_waiting_def)
 qed
 lemma held_unique:
-assumes "vt step s"
+assumes "vt s"
 and "holding s th1 cs"
 and "holding s th2 cs"
 shows "th1 = th2"
 proof -
 from prems show ?thesis
 by (simp add:Let_def)
 lemma step_v_hold_inv[elim_format]:
-"\<And>c t. \<lbrakk>vt step (V th cs # s);
+"\<And>c t. \<lbrakk>vt (V th cs # s);
 \<not> holding (wq s) t c; holding (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> next_th s th cs t \<and> c = cs"
 proof -
 fix c t
-assume vt: "vt step (V th cs # s)"
+assume vt: "vt (V th cs # s)"
 and nhd: "\<not> holding (wq s) t c"
 and hd: "holding (wq (V th cs # s)) t c"
 show "next_th s th cs t \<and> c = cs"
 proof(cases "c = cs")
 case False
 with True show ?thesis by auto
 qed
 qed
 lemma step_v_wait_inv[elim_format]:
-"\<And>t c. \<lbrakk>vt step (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
+"\<And>t c. \<lbrakk>vt (V th cs # s); \<not> waiting (wq (V th cs # s)) t c; waiting (wq s) t c
 \<rbrakk>
 \<Longrightarrow> (next_th s th cs t \<and> cs = c)"
 proof -
 fix t c
-assume vt: "vt step (V th cs # s)"
+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"
 show "next_th s th cs t \<and> cs = c"
 proof(cases "cs = c")
 case False
 with True show ?thesis by simp
 qed
 qed
 lemma step_v_not_wait[consumes 3]:
-"\<lbrakk>vt step (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"
+"\<lbrakk>vt (V th cs # s); next_th s th cs t; waiting (wq (V th cs # s)) t cs\<rbrakk> \<Longrightarrow> False"
 by (unfold next_th_def cs_waiting_def wq_def, auto simp:Let_def)
 lemma step_v_release:
-"\<lbrakk>vt step (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
+"\<lbrakk>vt (V th cs # s); holding (wq (V th cs # s)) th cs\<rbrakk> \<Longrightarrow> False"
 proof -
-assume vt: "vt step (V th cs # s)"
+assume vt: "vt (V th cs # s)"
 and hd: "holding (wq (V th cs # s)) th cs"
 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"
 qed
 qed
 qed
 lemma step_v_get_hold:
-"\<And>th'. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
+"\<And>th'. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) th' cs; next_th s th cs th'\<rbrakk> \<Longrightarrow> False"
 apply (unfold cs_holding_def next_th_def wq_def,
 auto simp:Let_def)
 proof -
 fix rest
-assume vt: "vt step (V th cs # s)"
+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)"
 have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"
 qed
 with ni show "False" by auto
 qed
 lemma step_v_release_inv[elim_format]:
-"\<And>c t. \<lbrakk>vt step (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow>
+"\<And>c t. \<lbrakk>vt (V th cs # s); \<not> holding (wq (V th cs # s)) t c; holding (wq s) t c\<rbrakk> \<Longrightarrow>
 c = cs \<and> t = th"
 apply (unfold cs_holding_def wq_def, auto simp:Let_def split:if_splits list.splits)
 proof -
 fix a list
-assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
+assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
 from step_back_step [OF vt] show "a = th"
 proof(cases)
 assume "holding s th cs" with eq_wq
 show ?thesis
 by (unfold s_holding_def wq_def, auto)
 qed
 next
 fix a list
-assume vt: "vt step (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
+assume vt: "vt (V th cs # s)" and eq_wq: "wq_fun (schs s) cs = a # list"
 from step_back_step [OF vt] show "a = th"
 proof(cases)
 assume "holding s th cs" with eq_wq
 show ?thesis
 by (unfold s_holding_def wq_def, auto)
 qed
 qed
 lemma step_v_waiting_mono:
-"\<And>t c. \<lbrakk>vt step (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
+"\<And>t c. \<lbrakk>vt (V th cs # s); waiting (wq (V th cs # s)) t c\<rbrakk> \<Longrightarrow> waiting (wq s) t c"
 proof -
 fix t c
 let ?s' = "(V th cs # s)"
-assume vt: "vt step ?s'"
+assume vt: "vt ?s'"
 and wt: "waiting (wq ?s') t c"
 show "waiting (wq s) t c"
 proof(cases "c = cs")
 case False
 assume neq_cs: "c \<noteq> cs"
 qed
 lemma step_depend_v:
 fixes th::thread
 assumes vt:
-"vt step (V th cs#s)"
+"vt (V th cs#s)"
 shows "
 depend (V th cs # s) =
 depend s - {(Cs cs, Th th)} -
 {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
 {(Cs cs, Th th') |th'.  next_th s th cs th'}"
 step_v_get_hold step_v_release_inv)
 apply (erule_tac step_v_not_wait, auto)
 done
 lemma step_depend_p:
-"vt step (P th cs#s) \<Longrightarrow>
+"vt (P th cs#s) \<Longrightarrow>
 depend (P th cs # s) =  (if (wq s cs = []) then depend s \<union> {(Cs cs, Th th)}
 else depend s \<union> {(Th th, Cs cs)})"
 apply(simp only: s_depend_def wq_def)
 apply (auto split:list.splits prod.splits simp:Let_def wq_def cs_waiting_def cs_holding_def)
 apply(case_tac "csa = cs", auto)
 lemma depend_target_th: "(Th th, x) \<in> depend (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
 by (unfold s_depend_def, auto)
 lemma acyclic_depend:
 fixes s
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "acyclic (depend s)"
 proof -
 from vt show ?thesis
 proof(induct)
 case (vt_cons s e)
 assume ih: "acyclic (depend s)"
 and stp: "step s e"
-and vt: "vt step s"
+and vt: "vt s"
 show ?case
 proof(cases e)
 case (Create th prio)
 with ih
 show ?thesis by (simp add:depend_create_unchanged)
 next
 case (Exit th)
 with ih show ?thesis by (simp add:depend_exit_unchanged)
 next
 case (V th cs)
-from V vt stp have vtt: "vt step (V th cs#s)" by auto
+from V vt stp have vtt: "vt (V th cs#s)" by auto
 from step_depend_v [OF this]
 have eq_de:
 "depend (e # s) =
 depend s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
 {(Cs cs, Th th') |th'. next_th s th cs th'}"
 have "step s (V th cs)" .
 thus ?thesis
 proof(cases)
 assume "holding s th cs"
 hence th_in: "th \<in> set (wq s cs)" and
-eq_hd: "th = hd (wq s cs)" by (unfold s_holding_def, auto)
+eq_hd: "th = hd (wq s cs)" unfolding s_holding_def wq_def by auto
 then obtain rest where
 eq_wq: "wq s cs = th#rest"
 by (cases "wq s cs", auto)
 show ?thesis
 proof(cases "rest = []")
 hence th_d: "(Th ?th', x) \<in> ?A" by simp
 from depend_target_th [OF this]
 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_depend_def s_waiting_def cs_waiting_def by simp
+unfolding s_depend_def s_waiting_def cs_waiting_def wq_def by simp
 hence "cs' = cs"
 proof(rule waiting_unique [OF vt])
 from eq_wq wq_distinct[OF vt, of cs]
 show "waiting s ?th' cs"
-apply (unfold s_waiting_def, auto)
+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 s cs = th # 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
-show "distinct rest \<and> set rest = set rest" by auto
+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
-show "distinct rest \<and> set rest = set rest" by auto
+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
 ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto
 show ?thesis by auto
 qed
 qed
 next
 case (P th cs)
-from P vt stp have vtt: "vt step (P th cs#s)" by auto
+from P vt stp have vtt: "vt (P th cs#s)" by auto
 from step_depend_p [OF this] P
 have "depend (e # s) =
 (if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else
 depend s \<union> {(Th th, Cs cs)})" (is "?L = ?R")
 by simp
 qed
 qed
 lemma finite_depend:
 fixes s
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "finite (depend s)"
 proof -
 from vt show ?thesis
 proof(induct)
 case (vt_cons s e)
 assume ih: "finite (depend s)"
 and stp: "step s e"
-and vt: "vt step s"
+and vt: "vt s"
 show ?case
 proof(cases e)
 case (Create th prio)
 with ih
 show ?thesis by (simp add:depend_create_unchanged)
 next
 case (Exit th)
 with ih show ?thesis by (simp add:depend_exit_unchanged)
 next
 case (V th cs)
-from V vt stp have vtt: "vt step (V th cs#s)" by auto
+from V vt stp have vtt: "vt (V th cs#s)" by auto
 from step_depend_v [OF this]
 have eq_de: "depend (e # s) =
 depend s - {(Cs cs, Th th)} - {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
 {(Cs cs, Th th') |th'. next_th s th cs th'}
 "
 qed
 qed
 ultimately show ?thesis by simp
 next
 case (P th cs)
-from P vt stp have vtt: "vt step (P th cs#s)" by auto
+from P vt stp have vtt: "vt (P th cs#s)" by auto
 from step_depend_p [OF this] P
 have "depend (e # s) =
 (if wq s cs = [] then depend s \<union> {(Cs cs, Th th)} else
 depend s \<union> {(Th th, Cs cs)})" (is "?L = ?R")
 by simp
 text {* Several useful lemmas *}
 lemma wf_dep_converse:
 fixes s
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "wf ((depend s)^-1)"
 proof(rule finite_acyclic_wf_converse)
 from finite_depend [OF vt]
 show "finite (depend s)" .
 next
 lemma th_chasing: "(Th th, Cs cs) \<in> depend (s::state) \<Longrightarrow> \<exists> th'. (Cs cs, Th th') \<in> depend s"
 by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
 lemma wq_threads:
 fixes s cs
-assumes vt: "vt step s"
+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)
 assume ih: "\<And>th cs. th \<in> set (wq s cs) \<Longrightarrow> th \<in> threads s"
 and stp: "step s e"
-and vt: "vt step s"
+and vt: "vt s"
 and h: "th \<in> set (wq (e # s) cs)"
 show ?case
 proof(cases e)
 case (Create th' prio)
 with ih h show ?thesis
 case vt_nil
 thus ?case by (auto simp:wq_def)
 qed
 qed
-lemma range_in: "\<lbrakk>vt step s; (Th th) \<in> Range (depend (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
+lemma range_in: "\<lbrakk>vt s; (Th th) \<in> Range (depend (s::state))\<rbrakk> \<Longrightarrow> th \<in> threads s"
 apply(unfold s_depend_def cs_waiting_def cs_holding_def)
 by (auto intro:wq_threads)
 lemma readys_v_eq:
 fixes th thread cs rest
-assumes vt: "vt step s"
+assumes vt: "vt s"
 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 prems show ?thesis
 apply (auto simp:readys_def)
-apply (case_tac "cs = csa", simp add:s_waiting_def)
+apply(simp add:s_waiting_def[folded wq_def])
 apply (erule_tac x = csa in allE)
 apply (simp add:s_waiting_def wq_def Let_def split:if_splits)
 apply (case_tac "csa = cs", simp)
 apply (erule_tac x = cs in allE)
+apply(auto simp add: s_waiting_def[folded wq_def] Let_def split: list.splits)
+apply(auto simp add: wq_def)
 apply (auto simp:s_waiting_def wq_def Let_def split:list.splits)
 proof -
 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] and eq_wq[folded wq_def]
+from wq_distinct[OF vt, 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
 qed
 qed
 lemma chain_building:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "node \<in> Domain (depend s) \<longrightarrow> (\<exists> th'. th' \<in> readys s \<and> (node, Th th') \<in> (depend s)^+)"
 proof -
 from wf_dep_converse [OF vt]
 have h: "wf ((depend s)\<inverse>)" .
 show ?thesis
 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
 with False have "Th th' \<in> Domain (depend s)"
-by (auto simp:readys_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
+by (auto simp:readys_def wq_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
 from ih [OF th'_d this]
 obtain th'' where
 th''_r: "th'' \<in> readys s" and
 th''_in: "(Th th', Th th'') \<in> (depend s)\<^sup>+" by auto
 from th'_d and th''_in
 qed
 qed
 lemma th_chain_to_ready:
 fixes s th
-assumes vt: "vt step 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> (depend 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 (depend s)"
-by (auto simp:readys_def s_waiting_def s_depend_def cs_waiting_def Domain_def)
+by (auto simp:readys_def s_waiting_def s_depend_def wq_def cs_waiting_def Domain_def)
 from chain_building [rule_format, OF vt this]
 show ?thesis by auto
 qed
 lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"
-by  (unfold s_waiting_def cs_waiting_def, auto)
+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 cs_holding_def, simp)
+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_depend: "\<lbrakk>vt step s; (n, n1) \<in> depend s; (n, n2) \<in> depend s\<rbrakk> \<Longrightarrow> n1 = n2"
+lemma unique_depend: "\<lbrakk>vt s; (n, n1) \<in> depend s; (n, n2) \<in> depend s\<rbrakk> \<Longrightarrow> n1 = n2"
 apply(unfold s_depend_def, auto, fold waiting_eq holding_eq)
 by(auto elim:waiting_unique holding_unique)
 lemma trancl_split: "(a, b) \<in> r^+ \<Longrightarrow> \<exists> c. (a, c) \<in> r"
 by (induct rule:trancl_induct, auto)
 lemma dchain_unique:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and th1_d: "(n, Th th1) \<in> (depend s)^+"
 and th1_r: "th1 \<in> readys s"
 and th2_d: "(n, Th th2) \<in> (depend s)^+"
 and th2_r: "th2 \<in> readys s"
 shows "th1 = th2"
 from trancl_split [OF this]
 obtain n where dd: "(Th th1, n) \<in> depend s" by auto
 then obtain cs where eq_n: "n = Cs cs"
 by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
 from dd eq_n have "th1 \<notin> readys s"
-by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+by (auto simp:readys_def s_depend_def wq_def s_waiting_def cs_waiting_def)
 with th1_r show ?thesis by auto
 next
 assume "(Th th2, Th th1) \<in> (depend s)\<^sup>+"
 from trancl_split [OF this]
 obtain n where dd: "(Th th2, n) \<in> depend s" by auto
 then obtain cs where eq_n: "n = Cs cs"
 by (auto simp:s_depend_def s_holding_def cs_holding_def cs_waiting_def wq_def dest:hd_np_in)
 from dd eq_n have "th2 \<notin> readys s"
-by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
 with th2_r show ?thesis by auto
 qed
 } thus ?thesis by auto
 qed
 lemma step_holdents_p_add:
 fixes th cs s
-assumes vt: "vt step (P th cs#s)"
+assumes vt: "vt (P th cs#s)"
 and "wq s cs = []"
 shows "holdents (P th cs#s) th = holdents s th \<union> {cs}"
 proof -
 from prems show ?thesis
 unfolding  holdents_def step_depend_p[OF vt] by auto
 qed
 lemma step_holdents_p_eq:
 fixes th cs s
-assumes vt: "vt step (P th cs#s)"
+assumes vt: "vt (P th cs#s)"
 and "wq s cs \<noteq> []"
 shows "holdents (P th cs#s) th = holdents s th"
 proof -
 from prems show ?thesis
 unfolding  holdents_def step_depend_p[OF vt] by auto
 qed
 lemma finite_holding:
 fixes s th cs
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "finite (holdents s th)"
 proof -
 let ?F = "\<lambda> (x, y). the_cs x"
 from finite_depend [OF vt]
 have "finite (depend s)" .
 ultimately show ?thesis by (unfold holdents_def, auto intro:finite_subset)
 qed
 lemma cntCS_v_dec:
 fixes s thread cs
-assumes vtv: "vt step (V thread cs#s)"
+assumes vtv: "vt (V thread cs#s)"
 shows "(cntCS (V thread cs#s) thread + 1) = cntCS s thread"
 proof -
 from step_back_step[OF vtv]
 have cs_in: "cs \<in> holdents s thread"
 apply (cases, unfold holdents_def s_depend_def, simp)
-by (unfold cs_holding_def s_holding_def, auto)
+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 (unfold holdents_def, unfold step_depend_v[OF vtv],
 auto simp:next_th_def)
 ultimately show ?thesis by (simp add:cntCS_def)
 qed
 lemma cnp_cnv_cncs:
 fixes s th
-assumes vt: "vt step s"
+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)
-assume vt: "vt step s"
+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
 proof(cases)
 with eq_e
 have "(th \<in> readys (e # s) \<or> th \<notin> threads (e # s)) =
 (th \<in> readys (s) \<or> th \<notin> threads (s))"
 apply (simp add:threads.simps readys_def)
 apply (subst s_waiting_def)
-apply (subst (1 2) wq_def)
 apply (simp add:Let_def)
 apply (subst s_waiting_def, simp)
-by (fold wq_def, simp)
+done
 with eq_cnp eq_cnv eq_cncs ih
 have ?thesis by simp
 } moreover {
 assume eq_th: "th = thread"
 with ih is_runing have " cntP s th = cntV s th + cntCS s th"
 next
 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> (depend s)\<^sup>+"
-from prems have vtp: "vt step (P thread cs#s)" by auto
+from prems have vtp: "vt (P thread cs#s)" by auto
 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
 proof
 assume "th \<in> readys (e#s)"
 hence "\<forall>cs. \<not> waiting (e # s) th cs" by (simp add:readys_def)
 from this[rule_format, of cs] have " \<not> waiting (e # s) th cs" .
 hence "th \<in> set (wq (e#s) cs) \<Longrightarrow> th = hd (wq (e#s) cs)"
-by (simp add:s_waiting_def)
+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]
 qed
 } ultimately show ?thesis by blast
 qed
 next
 case (thread_V thread cs)
-from prems have vtv: "vt step (V thread cs # s)" by auto
+from prems have vtv: "vt (V thread cs # s)" by auto
 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:s_holding_def)
+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
 show "distinct rest \<and> set rest = set rest" by auto
 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]
 and eq_wq show False by auto
 qed
-thus ?thesis by (simp add:s_waiting_def)
+thus ?thesis by (simp add:wq_def s_waiting_def)
 qed
 } moreover {
 assume neq_cs: "cs1 \<noteq> cs"
 have "\<not> waiting (e # s) thread cs1"
 proof -
 from runing_ready and is_runing
 have "thread \<in> readys s" by auto
 thus ?thesis by (simp add:readys_def)
 qed
 ultimately show ?thesis
-by (auto simp:s_waiting_def eq_e)
+by (auto simp:wq_def s_waiting_def eq_e)
 qed
 } ultimately show "\<not> waiting (e # s) thread cs1" by blast
 qed
 ultimately show ?thesis by (simp add:readys_def)
 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)
+by (insert wq_distinct[OF step_back_vt[OF vtv], 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)
 have "th \<notin> readys s"
 proof -
 from True eq_wq neq_th th_in
 show ?thesis
 apply (unfold readys_def s_waiting_def, auto)
-by (rule_tac x = cs in exI, auto)
+by (rule_tac x = cs in exI, auto simp add: wq_def)
 qed
 moreover have "th \<in> threads s"
 proof -
 from th_in eq_wq
 have "th \<in> set (wq s cs)" by simp
 qed
 qed
 lemma not_thread_cncs:
 fixes th s
-assumes vt: "vt step 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)
-assume vt: "vt step s"
+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
 proof(cases)
 qed
 next
 case (thread_P thread cs)
 assume eq_e: "e = P thread cs"
 and is_runing: "thread \<in> runing s"
-from prems have vtp: "vt step (P thread cs#s)" by auto
+from prems have vtp: "vt (P thread cs#s)" by auto
 have neq_th: "th \<noteq> thread"
 proof -
 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)
 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 prems have vtv: "vt step (V thread cs#s)" by auto
+from prems have vtv: "vt (V thread cs#s)" by auto
 from hold obtain rest
 where eq_wq: "wq s cs = thread # rest"
-by (case_tac "wq s cs", auto simp:s_holding_def)
+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"
 apply (auto simp:next_th_def)
 proof -
 assume ne: "rest \<noteq> []"
 auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)
 qed
 qed
 lemma eq_waiting: "waiting (wq (s::state)) th cs = waiting s th cs"
-by (auto simp:s_waiting_def cs_waiting_def)
+by (auto simp:s_waiting_def cs_waiting_def wq_def)
 lemma dm_depend_threads:
 fixes th s
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and in_dom: "(Th th) \<in> Domain (depend s)"
 shows "th \<in> threads s"
 proof -
 from in_dom obtain n where "(Th th, n) \<in> depend s" by auto
 moreover from depend_target_th[OF this] obtain cs where "n = Cs cs" by auto
 done
 lemma runing_unique:
 fixes th1 th2 s
-assumes vt: "vt step 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"
 from that [OF this] show ?thesis .
 qed
 lemma cnp_cnv_eq:
 fixes th s
-assumes "vt step s"
+assumes "vt s"
 and "th \<notin> threads s"
 shows "cntP s th = cntV s th"
 proof -
 from assms show ?thesis
 proof(induct)
 by (auto simp:cntP_def cntV_def count_def)
 next
 case (thread_exit thread)
 assume eq_e: "e = Exit thread"
 and not_holding: "holdents s thread = {}"
-have vt_s: "vt step s" by fact
+have vt_s: "vt s" by fact
 from finite_holding[OF vt_s] have "finite (holdents s thread)" .
 with not_holding have "cntCS s thread = 0" by (unfold cntCS_def, auto)
 moreover have "thread \<in> readys s" using thread_exit by (auto simp:runing_def)
 moreover note cnp_cnv_cncs[OF vt_s, of thread]
 ultimately have eq_thread: "cntP s thread = cntV s thread" by auto
 lemma eq_depend:
 "depend (wq s) = depend s"
 by (unfold cs_depend_def s_depend_def, auto)
 lemma count_eq_dependents:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and eq_pv: "cntP s th = cntV s th"
 shows "dependents (wq s) th = {}"
 proof -
 from cnp_cnv_cncs[OF vt] and eq_pv
 have "cntCS s th = 0"
 qed
 qed
 lemma dependents_threads:
 fixes s th
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "dependents (wq s) th \<subseteq> threads s"
 proof
 { fix th th'
 assume h: "th \<in> {th'a. (Th th'a, Th th') \<in> (depend (wq s))\<^sup>+}"
 have "Th th \<in> Domain (depend s)"
 by (unfold cs_dependents_def, simp)
 from hh [OF this] show "th1 \<in> threads s" .
 qed
 lemma finite_threads:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "finite (threads s)"
 proof -
 from vt show ?thesis
 proof(induct)
 case (vt_cons s e)
-assume vt: "vt step s"
+assume vt: "vt s"
 and step: "step s e"
 and ih: "finite (threads s)"
 from step
 show ?case
 proof(cases)
 next
 from fnt and seq show "finite (f ` B)" by auto
 qed
 lemma cp_le:
-assumes vt: "vt step s"
+assumes vt: "vt 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_dependents_def)
 show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+}))
 \<le> Max ((\<lambda>th. preced th s) ` threads s)"
 by (unfold cs_depend_def s_depend_def, auto simp:Domain_def)
 qed
 qed
 lemma le_cp:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "preced th s \<le> cp s th"
 proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
 show "Prc (original_priority th s) (birthtime th s)
 \<le> Max (insert (Prc (original_priority th s) (birthtime th s))
 ((\<lambda>th. Prc (original_priority th s) (birthtime th s)) ` dependents (wq s) th))"
 thus ?thesis by auto
 qed
 qed
 lemma max_cp_eq:
-assumes vt: "vt step s"
+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
 qed
 ultimately show ?thesis using eq_l by auto
 qed
 lemma max_cp_readys_threads_pre:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and np: "threads s \<noteq> {}"
 shows "Max (cp s ` readys s) = Max (cp s ` threads s)"
 proof(unfold max_cp_eq[OF vt])
 show "Max (cp s ` readys s) = Max ((\<lambda>th. preced th s) ` threads s)"
 proof -
 qed
 qed
 qed
 lemma max_cp_readys_threads:
-assumes vt: "vt step s"
+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)
 thus "th \<in> threads s"
 by (unfold readys_def, auto)
 qed
 lemma eq_holding: "holding (wq s) th cs = holding s th cs"
-apply (unfold s_holding_def cs_holding_def, simp)
+apply (unfold s_holding_def cs_holding_def wq_def, simp)
 done
 lemma f_image_eq:
 assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"
 shows "f ` A = g ` A"

changeset 298	f2e0d031a395
parent 294	bc5bf9e9ada2
child 309	e44c4055d430