--- a/prio/PrioG.thy Mon Feb 27 18:53:53 2012 +0000
+++ b/prio/PrioG.thy Tue Feb 28 13:13:32 2012 +0000
@@ -2,6 +2,7 @@
imports PrioGDef
begin
+
lemma runing_ready:
shows "runing s \<subseteq> readys s"
unfolding runing_def readys_def
@@ -415,26 +416,7 @@
and xz: "(x, z) \<in> r^+"
and neq: "y \<noteq> z"
shows "(y, z) \<in> r^+"
-proof -
- from xz and neq show ?thesis
- proof(induct)
- case (base ya)
- have "(x, ya) \<in> r" by fact
- from unique [OF xy this] have "y = ya" .
- with base show ?case by auto
- next
- case (step ya z)
- show ?case
- proof(cases "y = ya")
- case True
- from step True show ?thesis by simp
- next
- case False
- from step False
- show ?thesis by auto
- qed
- qed
-qed
+by (metis neq rtranclD tranclD unique xy xz)
lemma unique_base:
fixes r x y z
@@ -443,25 +425,7 @@
and xz: "(x, z) \<in> r^+"
and neq_yz: "y \<noteq> z"
shows "(y, z) \<in> r^+"
-proof -
- from xz neq_yz show ?thesis
- proof(induct)
- case (base ya)
- from xy unique base show ?case by auto
- next
- case (step ya z)
- show ?case
- proof(cases "y = ya")
- case True
- from True step show ?thesis by auto
- next
- case False
- from False step
- have "(y, ya) \<in> r\<^sup>+" by auto
- with step show ?thesis by auto
- qed
- qed
-qed
+by (metis neq_yz unique unique_minus xy xz)
lemma unique_chain:
fixes r x y z
@@ -672,25 +636,7 @@
"\<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 (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> []"
- proof(rule someI2)
- from wq_distinct[OF step_back_vt[OF vt], 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
- show "x \<noteq> []" by (case_tac x, auto)
- qed
- with ni show "False" by auto
-qed
+by (metis (lifting, full_types) List.member_def distinct.simps(2) hd_in_set member_rec(2) someI_ex step_back_vt wq_def wq_distinct)
lemma step_v_release_inv[elim_format]:
"\<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>
@@ -718,61 +664,7 @@
lemma step_v_waiting_mono:
"\<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 ?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"
- hence "waiting (wq ?s') t c = waiting (wq s) t c"
- by (unfold cs_waiting_def wq_def, auto simp:Let_def)
- with wt show ?thesis by simp
- next
- case True
- with wt show ?thesis
- apply (unfold cs_waiting_def wq_def, auto simp:Let_def split:list.splits)
- proof -
- fix a list
- 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]
- 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
- with not_in is_in show "t = a" by auto
- next
- fix list
- assume is_waiting: "waiting (wq (V th cs # s)) t cs"
- and eq_wq: "wq_fun (schs s) cs = t # list"
- hence "t \<in> set list"
- 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]
- 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]
- show False by auto
- qed
- qed
-qed
+by (metis abs2 block_pre cs_waiting_def event.simps(20))
lemma step_depend_v:
fixes th::thread
@@ -808,13 +700,7 @@
fixes A
assumes h: "\<And> x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x = y"
shows "A = {} \<or> (\<exists> a. A = {a})"
-proof(cases "A = {}")
- case True thus ?thesis by simp
-next
- case False then obtain a where "a \<in> A" by auto
- with h have "A = {a}" by auto
- thus ?thesis by simp
-qed
+by (metis assms insertCI nonempty_iff)
lemma depend_target_th: "(Th th, x) \<in> depend (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
by (unfold s_depend_def, auto)
@@ -1076,13 +962,7 @@
fixes 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
- from acyclic_depend[OF vt]
- show "acyclic (depend s)" .
-qed
+by (metis acyclic_depend assms finite_acyclic_wf_converse finite_depend)
lemma hd_np_in: "x \<in> set l \<Longrightarrow> hd l \<in> set l"
by (induct l, auto)
@@ -1203,31 +1083,17 @@
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
- apply (auto simp:readys_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, 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
+using assms
+apply (auto simp:readys_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)
+by (metis (lifting, full_types) distinct.simps(2) someI_ex wq_def wq_distinct)
lemma chain_building:
assumes vt: "vt s"
@@ -1404,51 +1270,8 @@
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)
- proof -
- fix rest
- assume dst: "distinct (rest::thread list)"
- and ne: "rest \<noteq> []"
- and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
- moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
- proof(rule someI2)
- from dst 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
- ultimately 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 dst 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
- ultimately
- show "(Cs cs, Th (hd (SOME q. distinct q \<and> set q = set rest))) \<in> depend s"
- by auto
- next
- fix rest
- assume dst: "distinct (rest::thread list)"
- and ne: "rest \<noteq> []"
- and hd_ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
- moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest"
- proof(rule someI2)
- from dst 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
- ultimately 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 dst 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
- ultimately show "False" by auto
- qed
+ apply (metis (lifting, full_types) hd_in_set hd_np_in someI_ex)
+ by (metis (lifting, full_types) hd_in_set hd_np_in someI_ex)
ultimately
have "holdents s thread = insert cs (holdents (V thread cs#s) thread)"
by auto
@@ -2308,106 +2131,20 @@
assumes le_ij: "i \<le> j"
and le_js: "j \<le> length s"
shows "length (down_to j i s) = j - i"
-proof -
- have "length (down_to j i s) = length (from_to i j (rev s))"
- by (unfold down_to_def, auto)
- also have "\<dots> = j - i"
- proof(rule length_from_to_in[OF le_ij])
- from le_js show "j \<le> length (rev s)" by simp
- qed
- finally show ?thesis .
-qed
+by (metis down_to_def le_ij le_js length_from_to_in length_rev)
lemma moment_head:
assumes le_it: "Suc i \<le> length t"
obtains e where "moment (Suc i) t = e#moment i t"
-proof -
- have "i \<le> Suc i" by simp
- from length_down_to_in [OF this le_it]
- have "length (down_to (Suc i) i t) = 1" by auto
- then obtain e where "down_to (Suc i) i t = [e]"
- apply (cases "(down_to (Suc i) i t)") by auto
- moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t"
- by (rule down_to_conc[symmetric], auto)
- 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
+by (metis assms moment_plus)
lemma cnp_cnv_eq:
fixes th s
assumes "vt s"
and "th \<notin> threads s"
shows "cntP s th = cntV s th"
-proof -
- from assms show ?thesis
- proof(induct)
- case (vt_cons s e)
- have ih: "th \<notin> threads s \<Longrightarrow> cntP s th = cntV s th" by fact
- have not_in: "th \<notin> threads (e # s)" by fact
- have "step s e" by fact
- thus ?case proof(cases)
- case (thread_create thread prio)
- assume eq_e: "e = Create thread prio"
- hence "thread \<in> threads (e#s)" by simp
- with not_in and eq_e have "th \<notin> threads s" by auto
- from ih [OF this] show ?thesis using eq_e
- 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 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
- show ?thesis
- proof(cases "th = thread")
- case True
- with eq_thread eq_e show ?thesis
- by (auto simp:cntP_def cntV_def count_def)
- next
- case False
- with not_in and eq_e have "th \<notin> threads s" by simp
- from ih[OF this] and eq_e show ?thesis
- by (auto simp:cntP_def cntV_def count_def)
- qed
- next
- case (thread_P thread cs)
- assume eq_e: "e = P thread cs"
- have "thread \<in> runing s" by fact
- with not_in eq_e have neq_th: "thread \<noteq> th"
- by (auto simp:runing_def readys_def)
- from not_in eq_e have "th \<notin> threads s" by simp
- from ih[OF this] and neq_th and eq_e show ?thesis
- by (auto simp:cntP_def cntV_def count_def)
- next
- case (thread_V thread cs)
- assume eq_e: "e = V thread cs"
- have "thread \<in> runing s" by fact
- with not_in eq_e have neq_th: "thread \<noteq> th"
- by (auto simp:runing_def readys_def)
- from not_in eq_e have "th \<notin> threads s" by simp
- from ih[OF this] and neq_th and eq_e show ?thesis
- by (auto simp:cntP_def cntV_def count_def)
- next
- case (thread_set thread prio)
- assume eq_e: "e = Set thread prio"
- and "thread \<in> runing s"
- hence "thread \<in> threads (e#s)"
- by (simp add:runing_def readys_def)
- with not_in and eq_e have "th \<notin> threads s" by auto
- from ih [OF this] show ?thesis using eq_e
- by (auto simp:cntP_def cntV_def count_def)
- qed
- next
- case vt_nil
- show ?case by (auto simp:cntP_def cntV_def count_def)
- qed
-qed
+by (metis (full_types) add_0_right assms(1) assms(2) cnp_cnv_cncs not_thread_cncs)
lemma eq_depend:
"depend (wq s) = depend s"
@@ -2515,43 +2252,8 @@
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 (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))"
- (is "?l \<le> Max (insert ?l ?A)")
- proof(cases "?A = {}")
- case False
- have "finite ?A" (is "finite (?f ` ?B)")
- proof -
- have "finite ?B"
- proof-
- have "finite {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+}"
- proof -
- let ?F = "\<lambda> (x, y). the_th x"
- have "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (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_depend[OF vt] have "finite (depend s)" .
- hence "finite ((depend (wq s))\<^sup>+)"
- apply (unfold finite_trancl)
- by (auto simp: s_depend_def cs_depend_def wq_def)
- thus ?thesis by auto
- qed
- ultimately show ?thesis by (auto intro:finite_subset)
- qed
- thus ?thesis by (simp add:cs_dependents_def)
- qed
- thus ?thesis by simp
- qed
- from Max_insert [OF this False, of ?l] show ?thesis by auto
- next
- case True
- thus ?thesis by auto
- qed
-qed
+apply(unfold cp_eq_cpreced preced_def cpreced_def, simp)
+by (metis (mono_tags) Max_ge assms dependents_threads finite_imageI finite_insert finite_threads insertI1 preced_def rev_finite_subset)
lemma max_cp_eq:
assumes vt: "vt s"