--- a/prio/PrioG.thy Sat Feb 11 09:14:14 2012 +0000
+++ b/prio/PrioG.thy Sat Feb 11 09:34:46 2012 +0000
@@ -18,14 +18,14 @@
proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)
fix thread s
assume h1: "(Cs cs, Th thread) \<notin> (depend s)\<^sup>+"
- and h2: "thread \<in> set (waiting_queue (schs s) cs)"
+ and h2: "thread \<in> set (wq_fun (schs s) cs)"
and h3: "thread \<in> runing s"
show "False"
proof -
- from h3 have "\<And> cs. thread \<in> set (waiting_queue (schs s) cs) \<Longrightarrow>
- thread = hd ((waiting_queue (schs s) cs))"
+ from h3 have "\<And> cs. thread \<in> set (wq_fun (schs s) cs) \<Longrightarrow>
+ thread = hd ((wq_fun (schs s) cs))"
by (simp add:runing_def readys_def s_waiting_def wq_def)
- from this [OF h2] have "thread = hd (waiting_queue (schs s) cs)" .
+ from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" .
with h2
have "(Cs cs, Th thread) \<in> (depend s)"
by (simp add:s_depend_def s_holding_def wq_def cs_holding_def)
@@ -81,8 +81,8 @@
apply (auto simp:wq_def Let_def split:if_splits)
proof -
fix q qs
- assume h1: "thread \<notin> set (waiting_queue (schs s) cs)"
- and h2: "q # qs = waiting_queue (schs s) cs"
+ 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)"
from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp
@@ -143,7 +143,7 @@
fix th qs
assume vt: "vt step (V th cs # s)"
and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"
- and eq_wq: "waiting_queue (schs s) cs = thread # 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]
@@ -193,7 +193,7 @@
qed
(* Wrong:
- lemma \<lbrakk>thread \<in> set (waiting_queue cs1 s); thread \<in> set (waiting_queue cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
+ lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"
*)
lemma waiting_unique_pre:
@@ -583,7 +583,7 @@
fix a list
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: "waiting_queue (schs s) cs = a # 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]
@@ -597,7 +597,7 @@
fix a list
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: "waiting_queue (schs s) cs = a # 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]
@@ -609,7 +609,7 @@
with t_ni and t_in show "t = hd (SOME q. distinct q \<and> set q = set list)" by auto
next
fix a list
- assume eq_wq: "waiting_queue (schs s) cs = a # list"
+ assume eq_wq: "wq_fun (schs s) cs = a # list"
from step_back_step[OF vt]
show "a = th"
proof(cases)
@@ -641,7 +641,7 @@
proof -
fix list
assume eq_wq[folded wq_def]:
- "waiting_queue (schs s) cs = hd (SOME q. distinct q \<and> set q = set list) # list"
+ "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"
@@ -670,7 +670,7 @@
proof -
fix rest
assume vt: "vt step (V th cs # s)"
- and eq_wq[folded wq_def]: " waiting_queue (schs s) cs = th # rest"
+ 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)"
@@ -693,7 +693,7 @@
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: "waiting_queue (schs s) cs = a # list"
+ assume vt: "vt step (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
@@ -702,7 +702,7 @@
qed
next
fix a list
- assume vt: "vt step (V th cs # s)" and eq_wq: "waiting_queue (schs s) cs = a # list"
+ assume vt: "vt step (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
@@ -733,7 +733,7 @@
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: "waiting_queue (schs s) cs = a # 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]
@@ -747,7 +747,7 @@
next
fix list
assume is_waiting: "waiting (wq (V th cs # s)) t cs"
- and eq_wq: "waiting_queue (schs s) cs = t # list"
+ 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 -
@@ -1125,25 +1125,25 @@
from h
show ?thesis
proof(unfold V wq_def)
- assume th_in: "th \<in> set (waiting_queue (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")
+ assume th_in: "th \<in> set (wq_fun (schs (V th' cs' # s)) cs)" (is "th \<in> set ?l")
show "th \<in> threads (V th' cs' # s)"
proof(cases "cs = cs'")
case False
- hence "?l = waiting_queue (schs s) cs" by (simp add:Let_def)
+ hence "?l = wq_fun (schs s) cs" by (simp add:Let_def)
with th_in have " th \<in> set (wq s cs)"
by (fold wq_def, simp)
from ih [OF this] show ?thesis by simp
next
case True
show ?thesis
- proof(cases "waiting_queue (schs s) cs'")
+ proof(cases "wq_fun (schs s) cs'")
case Nil
with h V show ?thesis
apply (auto simp:wq_def Let_def split:if_splits)
by (fold wq_def, drule_tac ih, simp)
next
case (Cons a rest)
- assume eq_wq: "waiting_queue (schs s) cs' = a # rest"
+ assume eq_wq: "wq_fun (schs s) cs' = a # rest"
with h V show ?thesis
apply (auto simp:Let_def wq_def split:if_splits)
proof -
@@ -1156,10 +1156,10 @@
show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest"
by auto
qed
- with eq_wq th_in have "th \<in> set (waiting_queue (schs s) cs')" by auto
+ with eq_wq th_in have "th \<in> set (wq_fun (schs s) cs')" by auto
from ih[OF this[folded wq_def]] show "th \<in> threads s" .
next
- assume th_in: "th \<in> set (waiting_queue (schs s) cs)"
+ assume th_in: "th \<in> set (wq_fun (schs s) cs)"
from ih[OF this[folded wq_def]]
show "th \<in> threads s" .
qed
@@ -1210,7 +1210,7 @@
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: "waiting_queue (schs s) cs = thread # 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]
@@ -1550,9 +1550,9 @@
apply (rule_tac hh, clarify)
apply (intro iffI allI, clarify)
apply (erule_tac x = csa in allE, auto)
- apply (subgoal_tac "waiting_queue (schs s) cs \<noteq> []", auto)
+ apply (subgoal_tac "wq_fun (schs s) cs \<noteq> []", auto)
apply (erule_tac x = cs in allE, auto)
- by (case_tac "(waiting_queue (schs s) cs)", auto)
+ by (case_tac "(wq_fun (schs s) cs)", auto)
moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th"
apply (simp add:cntCS_def holdents_def)
by (unfold step_depend_p [OF vtp], auto)
@@ -1807,7 +1807,7 @@
apply (auto simp:eq_e readys_def s_waiting_def wq_def
Let_def next_th_def)
proof -
- assume eq_wq: "waiting_queue (schs s) cs = thread # rest"
+ 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]])
@@ -1816,13 +1816,13 @@
qed
next
fix csa
- assume eq_wq: "waiting_queue (schs s) cs = thread # rest"
+ assume eq_wq: "wq_fun (schs s) cs = thread # rest"
and t_in: "?t \<in> set rest"
and neq_cs: "csa \<noteq> cs"
- and t_in': "?t \<in> set (waiting_queue (schs s) csa)"
- show "?t = hd (waiting_queue (schs s) csa)"
+ 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 (waiting_queue (schs s) csa)"
+ { assume neq_hd': "?t \<noteq> hd (wq_fun (schs s) csa)"
from wq_distinct[OF step_back_vt[OF vtv], of cs] and
eq_wq[folded wq_def] and t_in eq_wq
have "?t \<noteq> thread" by auto