--- a/prio/CpsG.thy Sat Feb 11 19:39:50 2012 +0000
+++ b/prio/CpsG.thy Sun Feb 12 04:45:20 2012 +0000
@@ -4,14 +4,14 @@
lemma not_thread_holdents:
fixes th s
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and not_in: "th \<notin> threads s"
shows "holdents s th = {}"
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> holdents s th = {}"
and stp: "step s e"
and not_in: "th \<notin> threads (e # s)"
@@ -49,7 +49,7 @@
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
@@ -77,10 +77,10 @@
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)
@@ -128,7 +128,7 @@
lemma next_th_neq:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and nt: "next_th s th cs th'"
shows "th' \<noteq> th"
proof -
@@ -167,7 +167,7 @@
by auto
lemma wf_depend:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "wf (depend s)"
proof(rule finite_acyclic_wf)
from finite_depend[OF vt] show "finite (depend s)" .
@@ -256,7 +256,7 @@
by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
lemma child_unique:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and ch1: "(Th th, Th th1) \<in> child s"
and ch2: "(Th th, Th th2) \<in> child s"
shows "th1 = th2"
@@ -329,7 +329,7 @@
by (unfold child_def, auto)
lemma wf_child:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "wf (child s)"
proof(rule wf_subset)
from wf_trancl[OF wf_depend[OF vt]]
@@ -339,7 +339,7 @@
qed
lemma depend_child_pre:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows
"(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
proof -
@@ -371,7 +371,7 @@
qed
qed
-lemma depend_child: "\<lbrakk>vt step s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
+lemma depend_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
by (insert depend_child_pre, auto)
lemma child_depend_p:
@@ -392,7 +392,7 @@
qed
lemma child_depend_eq:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows
"((Th th1, Th th2) \<in> (child s)^+) =
((Th th1, Th th2) \<in> (depend s)^+)"
@@ -400,7 +400,7 @@
lemma children_no_dep:
fixes s th th1 th2 th3
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and ch1: "(Th th1, Th th) \<in> child s"
and ch2: "(Th th2, Th th) \<in> child s"
and ch3: "(Th th1, Th th2) \<in> (depend s)^+"
@@ -433,7 +433,7 @@
qed
lemma unique_depend_p:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and dp1: "(n, n1) \<in> (depend s)^+"
and dp2: "(n, n2) \<in> (depend s)^+"
and neq: "n1 \<noteq> n2"
@@ -445,7 +445,7 @@
lemma dependents_child_unique:
fixes s th th1 th2 th3
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and ch1: "(Th th1, Th th) \<in> child s"
and ch2: "(Th th2, Th th) \<in> child s"
and dp1: "th3 \<in> dependents s th1"
@@ -472,7 +472,7 @@
lemma cp_rec:
fixes s th
- assumes vt: "vt step s"
+ assumes vt: "vt s"
shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
proof(unfold cp_eq_cpreced_f cpreced_def)
let ?f = "(\<lambda>th. preced th s)"
@@ -625,7 +625,7 @@
locale step_set_cps =
fixes s' th prio s
defines s_def : "s \<equiv> (Set th prio#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
context step_set_cps
begin
@@ -936,12 +936,12 @@
end
lemma next_waiting:
- assumes vt: "vt step s"
+ assumes vt: "vt s"
and nxt: "next_th s th cs th'"
shows "waiting s th' cs"
proof -
from assms show ?thesis
- apply (auto simp:next_th_def s_waiting_def)
+ apply (auto simp:next_th_def s_waiting_def[folded wq_def])
proof -
fix rest
assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
@@ -994,7 +994,7 @@
locale step_v_cps =
fixes s' th cs s
defines s_def : "s \<equiv> (V th cs#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
locale step_v_cps_nt = step_v_cps +
fixes th'
@@ -1054,7 +1054,7 @@
proof -
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
have "(Th th', Cs cs) \<in> depend s'"
- by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+ by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
show ?thesis by simp
qed
@@ -1072,7 +1072,7 @@
proof -
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
have "(Th th', Cs cs) \<in> depend s'"
- by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+ by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
show ?thesis .
qed
@@ -1115,7 +1115,7 @@
proof -
from step_back_step[OF vt_s[unfolded s_def]]
have "(Cs cs, Th th) \<in> depend s'"
- by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+ by(cases, auto simp: wq_def s_depend_def cs_holding_def s_holding_def)
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
show ?thesis by simp
qed
@@ -1126,7 +1126,7 @@
have "th \<in> readys s'" by (cases, simp add:runing_def)
moreover note eq_z
ultimately show False
- 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)
qed
next
show "y \<noteq> Th th'"
@@ -1137,14 +1137,14 @@
proof -
from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
have "(Th th', Cs cs) \<in> depend s'"
- by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+ by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
show ?thesis .
qed
with ztp have cs_i: "(Cs cs, Th th'') \<in> (depend s')\<^sup>+" by simp
from step_back_step[OF vt_s[unfolded s_def]]
have cs_th: "(Cs cs, Th th) \<in> depend s'"
- by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+ by(cases, auto simp: s_depend_def wq_def cs_holding_def s_holding_def)
have "(Cs cs, Th th'') \<notin> depend s'"
proof
assume "(Cs cs, Th th'') \<in> depend s'"
@@ -1165,7 +1165,7 @@
moreover from step_back_step[OF vt_s[unfolded s_def]]
have "th \<in> readys s'" by (cases, simp add:runing_def)
ultimately show False
- 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)
qed
qed
with depend_s yz have "(y, z) \<in> depend s" by auto
@@ -1223,7 +1223,7 @@
assume "holding s' th cs"
then obtain rest where
eq_wq: "wq s' cs = th#rest"
- apply (unfold s_holding_def)
+ apply (unfold s_holding_def wq_def[symmetric])
by (case_tac "(wq s' cs)", auto)
with h1 h2 have ne: "rest \<noteq> []" by auto
with eq_wq
@@ -1351,7 +1351,7 @@
locale step_P_cps =
fixes s' th cs s
defines s_def : "s \<equiv> (P th cs#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
locale step_P_cps_ne =step_P_cps +
assumes ne: "wq s' cs \<noteq> []"
@@ -1814,7 +1814,7 @@
locale step_create_cps =
fixes s' th prio s
defines s_def : "s \<equiv> (Create th prio#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
context step_create_cps
begin
@@ -1902,7 +1902,7 @@
locale step_exit_cps =
fixes s' th prio s
defines s_def : "s \<equiv> (Exit th#s')"
- assumes vt_s: "vt step s"
+ assumes vt_s: "vt s"
context step_exit_cps
begin
@@ -1930,7 +1930,7 @@
assume "th \<in> runing s'"
with bk show ?thesis
apply (unfold runing_def readys_def s_waiting_def s_depend_def)
- by (auto simp:cs_waiting_def)
+ by (auto simp:cs_waiting_def wq_def)
qed
qed
have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"