--- a/CpsG.thy~ Fri Dec 18 22:47:32 2015 +0800
+++ b/CpsG.thy~ Tue Dec 22 23:13:31 2015 +0800
@@ -6,24 +6,37 @@
imports PrioG Max RTree
begin
+text {* @{text "the_preced"} is also the same as @{text "preced"}, the only
+ difference is the order of arguemts. *}
definition "the_preced s th = preced th s"
+text {* @{term "the_thread"} extracts thread out of RAG node. *}
fun the_thread :: "node \<Rightarrow> thread" where
"the_thread (Th th) = th"
+text {* The following @{text "wRAG"} is the waiting sub-graph of @{text "RAG"}. *}
definition "wRAG (s::state) = {(Th th, Cs cs) | th cs. waiting s th cs}"
+text {* The following @{text "hRAG"} is the holding sub-graph of @{text "RAG"}. *}
definition "hRAG (s::state) = {(Cs cs, Th th) | th cs. holding s th cs}"
+text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}
+lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
+ by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv
+ s_holding_abv cs_RAG_def, auto)
+
+text {*
+ The following @{text "tRAG"} is the thread-graph derived from @{term "RAG"}.
+ It characterizes the dependency between threads when calculating current
+ precedences. It is defined as the composition of the above two sub-graphs,
+ names @{term "wRAG"} and @{term "hRAG"}.
+ *}
definition "tRAG s = wRAG s O hRAG s"
+(* ccc *)
+
definition "cp_gen s x =
Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"
-(* ccc *)
-
-lemma RAG_split: "RAG s = (wRAG s \<union> hRAG s)"
- by (unfold s_RAG_abv wRAG_def hRAG_def s_waiting_abv
- s_holding_abv cs_RAG_def, auto)
lemma tRAG_alt_def:
"tRAG s = {(Th th1, Th th2) | th1 th2.
@@ -363,11 +376,6 @@
from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
qed
-end
-
-context valid_trace
-begin
-
lemma sgv_wRAG: "single_valued (wRAG s)"
using waiting_unique[OF vt]
by (unfold single_valued_def wRAG_def, auto)
@@ -395,8 +403,19 @@
lemma rtree_RAG: "rtree (RAG s)"
using sgv_RAG acyclic_RAG[OF vt]
by (unfold rtree_def rtree_axioms_def sgv_def, auto)
+end
-end
+
+sublocale valid_trace < rtree_RAG: rtree "RAG s"
+proof
+ show "single_valued (RAG s)"
+ apply (intro_locales)
+ by (unfold single_valued_def,
+ auto intro:unique_RAG[OF vt])
+
+ show "acyclic (RAG s)"
+ by (rule acyclic_RAG[OF vt])
+qed
sublocale valid_trace < rtree_s: rtree "tRAG s"
proof(unfold_locales)
@@ -478,7 +497,6 @@
finally show ?thesis by simp
qed
-
context valid_trace
begin
@@ -560,363 +578,7 @@
end
-(* ccc *)
-
-
-
-(* obvious lemma *)
-
-lemma wf_RAG:
- assumes vt: "vt s"
- shows "wf (RAG s)"
-proof(rule finite_acyclic_wf)
- from finite_RAG[OF vt] show "finite (RAG s)" .
-next
- from acyclic_RAG[OF vt] show "acyclic (RAG s)" .
-qed
-
-definition child :: "state \<Rightarrow> (node \<times> node) set"
- where "child s \<equiv>
- {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
-
-definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"
- where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"
-
-lemma children_def2:
- "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"
-unfolding child_def children_def by simp
-
-lemma children_dependants:
- "children s th \<subseteq> dependants (wq s) th"
- unfolding children_def2
- unfolding cs_dependants_def
- by (auto simp add: eq_RAG)
-
-lemma child_unique:
- 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"
-using ch1 ch2
-proof(unfold child_def, clarsimp)
- fix cs csa
- assume h1: "(Th th, Cs cs) \<in> RAG s"
- and h2: "(Cs cs, Th th1) \<in> RAG s"
- and h3: "(Th th, Cs csa) \<in> RAG s"
- and h4: "(Cs csa, Th th2) \<in> RAG s"
- from unique_RAG[OF vt h1 h3] have "cs = csa" by simp
- with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp
- from unique_RAG[OF vt h2 this]
- show "th1 = th2" by simp
-qed
-
-lemma RAG_children:
- assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"
- shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"
-proof -
- from h show ?thesis
- proof(induct rule: tranclE)
- fix c th2
- assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"
- and h2: "(c, Th th2) \<in> RAG s"
- from h2 obtain cs where eq_c: "c = Cs cs"
- by (case_tac c, auto simp:s_RAG_def)
- show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
- proof(rule tranclE[OF h1])
- fix ca
- assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"
- and h4: "(ca, c) \<in> RAG s"
- show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"
- proof -
- from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"
- by (case_tac ca, auto simp:s_RAG_def)
- from eq_ca h4 h2 eq_c
- have "th3 \<in> children s th2" by (auto simp:children_def child_def)
- moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp
- ultimately show ?thesis by auto
- qed
- next
- assume "(Th th1, c) \<in> RAG s"
- with h2 eq_c
- have "th1 \<in> children s th2"
- by (auto simp:children_def child_def)
- thus ?thesis by auto
- qed
- next
- assume "(Th th1, Th th2) \<in> RAG s"
- thus ?thesis
- by (auto simp:s_RAG_def)
- qed
-qed
-
-lemma sub_child: "child s \<subseteq> (RAG s)^+"
- by (unfold child_def, auto)
-
-lemma wf_child:
- assumes vt: "vt s"
- shows "wf (child s)"
-apply(rule wf_subset)
-apply(rule wf_trancl[OF wf_RAG[OF vt]])
-apply(rule sub_child)
-done
-
-lemma RAG_child_pre:
- assumes vt: "vt s"
- shows
- "(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
-proof -
- from wf_trancl[OF wf_RAG[OF vt]]
- have wf: "wf ((RAG s)^+)" .
- show ?thesis
- proof(rule wf_induct[OF wf, of ?P], clarsimp)
- fix th'
- assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>
- (Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"
- and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"
- show "(Th th, Th th') \<in> (child s)\<^sup>+"
- proof -
- from RAG_children[OF h]
- have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .
- thus ?thesis
- proof
- assume "th \<in> children s th'"
- thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
- next
- assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"
- then obtain th3 where th3_in: "th3 \<in> children s th'"
- and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto
- from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)
- from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp
- with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)
- qed
- qed
- qed
-qed
-
-lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
- by (insert RAG_child_pre, auto)
-
-lemma child_RAG_p:
- assumes "(n1, n2) \<in> (child s)^+"
- shows "(n1, n2) \<in> (RAG s)^+"
-proof -
- from assms show ?thesis
- proof(induct)
- case (base y)
- with sub_child show ?case by auto
- next
- case (step y z)
- assume "(y, z) \<in> child s"
- with sub_child have "(y, z) \<in> (RAG s)^+" by auto
- moreover have "(n1, y) \<in> (RAG s)^+" by fact
- ultimately show ?case by auto
- qed
-qed
-
-text {* (* ddd *)
-*}
-lemma child_RAG_eq:
- assumes vt: "vt s"
- shows "(Th th1, Th th2) \<in> (child s)^+ \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"
- by (auto intro: RAG_child[OF vt] child_RAG_p)
-
-text {* (* ddd *)
-*}
-lemma children_no_dep:
- fixes s th th1 th2 th3
- 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> (RAG s)^+"
- shows "False"
-proof -
- from RAG_child[OF vt ch3]
- have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .
- thus ?thesis
- proof(rule converse_tranclE)
- assume "(Th th1, Th th2) \<in> child s"
- from child_unique[OF vt ch1 this] have "th = th2" by simp
- with ch2 have "(Th th2, Th th2) \<in> child s" by simp
- with wf_child[OF vt] show ?thesis by auto
- next
- fix c
- assume h1: "(Th th1, c) \<in> child s"
- and h2: "(c, Th th2) \<in> (child s)\<^sup>+"
- from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)
- with h1 have "(Th th1, Th th3) \<in> child s" by simp
- from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp
- with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp
- with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto
- moreover have "wf ((child s)\<^sup>+)"
- proof(rule wf_trancl)
- from wf_child[OF vt] show "wf (child s)" .
- qed
- ultimately show False by auto
- qed
-qed
-
-text {* (* ddd *)
-*}
-lemma unique_RAG_p:
- assumes vt: "vt s"
- and dp1: "(n, n1) \<in> (RAG s)^+"
- and dp2: "(n, n2) \<in> (RAG s)^+"
- and neq: "n1 \<noteq> n2"
- shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"
-proof(rule unique_chain [OF _ dp1 dp2 neq])
- from unique_RAG[OF vt]
- show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto
-qed
-
-text {* (* ddd *)
-*}
-lemma dependants_child_unique:
- fixes s th th1 th2 th3
- 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> dependants s th1"
- and dp2: "th3 \<in> dependants s th2"
-shows "th1 = th2"
-proof -
- { assume neq: "th1 \<noteq> th2"
- from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+"
- by (simp add:s_dependants_def eq_RAG)
- from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+"
- by (simp add:s_dependants_def eq_RAG)
- from unique_RAG_p[OF vt dp1 dp2] and neq
- 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 children_no_dep[OF vt ch1 ch2 this] show ?thesis .
- next
- assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"
- from children_no_dep[OF vt ch2 ch1 this] show ?thesis .
- qed
- } thus ?thesis by auto
-qed
-
-lemma RAG_plus_elim:
- assumes "vt s"
- fixes x
- assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"
- shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"
- using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]
- apply (unfold children_def)
- by (metis assms(2) children_def RAG_children eq_RAG)
-
-text {* (* ddd *)
-*}
-lemma dependants_expand:
- assumes "vt s"
- shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"
-apply(simp add: image_def)
-unfolding cs_dependants_def
-apply(auto)
-apply (metis assms RAG_plus_elim mem_Collect_eq)
-apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')
-by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)
-
-lemma finite_children:
- assumes "vt s"
- shows "finite (children s th)"
- using children_dependants dependants_threads[OF assms] finite_threads[OF assms]
- by (metis rev_finite_subset)
-
-lemma finite_dependants:
- assumes "vt s"
- shows "finite (dependants (wq s) th')"
- using dependants_threads[OF assms] finite_threads[OF assms]
- by (metis rev_finite_subset)
-
-abbreviation
- "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"
-
-abbreviation
- "cpreceds s ths \<equiv> (cp s) ` ths"
-
-lemma Un_compr:
- "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"
-by auto
-
-lemma in_disj:
- shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"
-by metis
-
-lemma UN_exists:
- shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"
-by auto
-
-text {* (* ddd *)
- This is the recursive equation used to compute the current precedence of
- a thread (the @{text "th"}) here.
-*}
-lemma cp_rec:
- fixes s th
- assumes vt: "vt s"
- shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
-proof(cases "children s th = {}")
- case True
- show ?thesis
- unfolding cp_eq_cpreced cpreced_def
- by (subst dependants_expand[OF `vt s`]) (simp add: True)
-next
- case False
- show ?thesis (is "?LHS = ?RHS")
- proof -
- have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"
- by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])
-
- have not_emptyness_facts[simp]:
- "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"
- using False dependants_expand[OF assms] by(auto simp only: Un_empty)
-
- have finiteness_facts[simp]:
- "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"
- by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])
-
- (* expanding definition *)
- have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"
- unfolding eq_cp by (simp add: Un_compr)
-
- (* moving Max in *)
- also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"
- by (simp add: Max_Un)
-
- (* expanding dependants *)
- also have "\<dots> = max (Max {preced th s})
- (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"
- by (subst dependants_expand[OF `vt s`]) (simp)
-
- (* moving out big Union *)
- also have "\<dots> = max (Max {preced th s})
- (Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"
- by simp
-
- (* moving in small union *)
- also have "\<dots> = max (Max {preced th s})
- (Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"
- by (simp add: in_disj)
-
- (* moving in preceds *)
- also have "\<dots> = max (Max {preced th s})
- (Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))"
- by (simp add: UN_exists)
-
- (* moving in Max *)
- also have "\<dots> = max (Max {preced th s})
- (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))"
- by (subst Max_Union) (auto simp add: image_image)
-
- (* folding cp + moving out Max *)
- also have "\<dots> = ?RHS"
- unfolding eq_cp by (simp add: Max_insert)
-
- finally show "?LHS = ?RHS" .
- qed
-qed
-
+(* keep *)
lemma next_th_holding:
assumes vt: "vt s"
and nxt: "next_th s th cs th'"
@@ -1006,6 +668,16 @@
the legitimacy of @{text "s"} can be derived. *}
assumes vt_s: "vt s"
+sublocale step_set_cps < vat_s : valid_trace "s"
+proof
+ from vt_s show "vt s" .
+qed
+
+sublocale step_set_cps < vat_s' : valid_trace "s'"
+proof
+ from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
+qed
+
context step_set_cps
begin
@@ -1015,7 +687,6 @@
*}
lemma eq_preced:
- fixes th'
assumes "th' \<noteq> th"
shows "preced th' s = preced th' s'"
proof -
@@ -1089,7 +760,8 @@
hence "th \<in> runing s'" by (cases, simp)
thus ?thesis by (simp add:readys_def runing_def)
qed
- from readys_in_no_subtree[OF step_back_vt[OF vt_s[unfolded s_def]] this assms(1)]
+ find_theorems readys subtree
+ from vat_s'.readys_in_no_subtree[OF this assms(1)]
show ?thesis by blast
qed
@@ -1118,40 +790,26 @@
-- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}
assumes vt_s: "vt s"
-context step_v_cps
-begin
-
-lemma rtree_RAGs: "rtree (RAG s)"
+sublocale step_v_cps < vat_s : valid_trace "s"
proof
- show "single_valued (RAG s)"
- apply (intro_locales)
- by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
-
- show "acyclic (RAG s)"
- by (rule acyclic_RAG[OF vt_s])
+ from vt_s show "vt s" .
qed
-lemma rtree_RAGs': "rtree (RAG s')"
+sublocale step_v_cps < vat_s' : valid_trace "s'"
proof
- show "single_valued (RAG s')"
- apply (intro_locales)
- by (unfold single_valued_def,
- auto intro:unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
-
- show "acyclic (RAG s')"
- by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
+ from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
qed
-lemmas vt_s' = step_back_vt[OF vt_s[unfolded s_def]]
+context step_v_cps
+begin
lemma ready_th_s': "th \<in> readys s'"
using step_back_step[OF vt_s[unfolded s_def]]
by (cases, simp add:runing_def)
-
lemma ancestors_th: "ancestors (RAG s') (Th th) = {}"
proof -
- from readys_root[OF vt_s' ready_th_s']
+ from vat_s'.readys_root[OF ready_th_s']
show ?thesis
by (unfold root_def, simp)
qed
@@ -1174,9 +832,8 @@
lemma ancestors_cs:
"ancestors (RAG s') (Cs cs) = {Th th}"
proof -
- find_theorems ancestors
have "ancestors (RAG s') (Cs cs) = ancestors (RAG s') (Th th) \<union> {Th th}"
- proof(rule RTree.rtree.ancestors_accum[OF rtree_RAGs'])
+ proof(rule vat_s'.rtree_RAG.ancestors_accum)
from vt_s[unfolded s_def]
have " PIP s' (V th cs)" by (cases, simp)
thus "(Cs cs, Th th) \<in> RAG s'"
@@ -1194,7 +851,6 @@
end
-
text {*
The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation,
which represents the case when there is another thread @{text "th'"}
@@ -1249,13 +905,13 @@
*)
lemma sub_RAGs': "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s'"
- using next_th_RAG[OF vt_s' nt] .
+ using next_th_RAG[OF vat_s'.vt nt] .
lemma ancestors_th':
"ancestors (RAG s') (Th th') = {Th th, Cs cs}"
proof -
have "ancestors (RAG s') (Th th') = ancestors (RAG s') (Cs cs) \<union> {Cs cs}"
- proof(rule RTree.rtree.ancestors_accum[OF rtree_RAGs'])
+ proof(rule vat_s'.rtree_RAG.ancestors_accum)
from sub_RAGs' show "(Th th', Cs cs) \<in> RAG s'" by auto
qed
thus ?thesis using ancestors_th ancestors_cs by auto
@@ -1386,7 +1042,8 @@
lemma subtree_th:
"subtree (RAG s) (Th th) = subtree (RAG s') (Th th) - {Cs cs}"
-proof(unfold RAG_s, fold subtree_cs, rule RTree.rtree.subtree_del_inside[OF rtree_RAGs'])
+find_theorems "subtree" "_ - _" RAG
+proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside)
from edge_of_th
show "(Cs cs, Th th) \<in> edges_in (RAG s') (Th th)"
by (unfold edges_in_def, auto simp:subtree_def)
@@ -1401,18 +1058,8 @@
shows "cp s th' = cp s' th'"
using cp_kept_1 cp_kept_2
by (cases "th' = th", auto)
-
end
-find_theorems "_`_" "\<Union> _"
-
-find_theorems "Max" "\<Union> _"
-
-find_theorems wf RAG
-
-thm wf_def
-
-thm image_Union
locale step_P_cps =
fixes s' th cs s
@@ -1429,7 +1076,6 @@
from step_back_vt[OF vt_s[unfolded s_def]] show "vt s'" .
qed
-
context step_P_cps
begin
@@ -1442,7 +1088,7 @@
qed
lemma root_th: "root (RAG s') (Th th)"
- using readys_root[OF vat_s'.vt readys_th] .
+ using readys_root[OF readys_th] .
lemma in_no_others_subtree:
assumes "th' \<noteq> th"
@@ -1873,7 +1519,8 @@
qed auto
have neq_th_a: "th_a \<noteq> th"
proof -
- from readys_in_no_subtree[OF vat_s'.vt th_ready assms]
+ find_theorems readys subtree s'
+ from vat_s'.readys_in_no_subtree[OF th_ready assms]
have "(Th th) \<notin> subtree (RAG s') (Th th')" .
with tRAG_subtree_RAG[of s' "Th th'"]
have "(Th th) \<notin> subtree (tRAG s') (Th th')" by auto
--- a/ExtGG.thy Fri Dec 18 22:47:32 2015 +0800
+++ b/ExtGG.thy Tue Dec 22 23:13:31 2015 +0800
@@ -1,5 +1,5 @@
theory ExtGG
-imports PrioG
+imports PrioG CpsG
begin
lemma birth_time_lt: "s \<noteq> [] \<Longrightarrow> last_set th s < length s"
@@ -34,44 +34,24 @@
and highest: "preced th s = Max ((cp s)`threads s)"
and preced_th: "preced th s = Prc prio tm"
+sublocale highest_gen < vat_s: valid_trace "s"
+ by (unfold_locales, insert vt_s, simp)
+
context highest_gen
begin
-
-
lemma lt_tm: "tm < length s"
by (insert preced_tm_lt[OF threads_s preced_th], simp)
-lemma eq_cp_s_th: "cp s th = preced th s"
+lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")
proof -
- from highest and max_cp_eq[OF vt_s]
- have is_max: "preced th s = Max ((\<lambda>th. preced th s) ` threads s)" by simp
- have sbs: "({th} \<union> dependants (wq s) th) \<subseteq> threads s"
- proof -
- from threads_s and dependants_threads[OF vt_s, of th]
- show ?thesis by auto
- qed
- show ?thesis
- proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)
- show "preced th s \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)" by simp
- next
- fix y
- assume "y \<in> (\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th)"
- then obtain th1 where th1_in: "th1 \<in> ({th} \<union> dependants (wq s) th)"
- and eq_y: "y = preced th1 s" by auto
- show "y \<le> preced th s"
- proof(unfold is_max, rule Max_ge)
- from finite_threads[OF vt_s]
- show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
- next
- from sbs th1_in and eq_y
- show "y \<in> (\<lambda>th. preced th s) ` threads s" by auto
- qed
- next
- from sbs and finite_threads[OF vt_s]
- show "finite ((\<lambda>th. preced th s) ` ({th} \<union> dependants (wq s) th))"
- by (auto intro:finite_subset)
- qed
+ have "?L \<le> ?R"
+ by (unfold highest, rule Max_ge,
+ auto simp:threads_s finite_threads[OF vt_s])
+ moreover have "?R \<le> ?L"
+ by (unfold vat_s.cp_rec, rule Max_ge,
+ auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)
+ ultimately show ?thesis by auto
qed
lemma highest_cp_preced: "cp s th = Max ((\<lambda> th'. preced th' s) ` threads s)"
@@ -117,18 +97,28 @@
qed
qed
-context extend_highest_gen
-begin
-thm extend_highest_gen_axioms_def
+locale red_extend_highest_gen = extend_highest_gen +
+ fixes i::nat
-lemma red_moment:
- "extend_highest_gen s th prio tm (moment i t)"
+sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"
apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
by (unfold highest_gen_def, auto dest:step_back_vt_app)
-lemma ind [consumes 0, case_names Nil Cons, induct type]:
+
+context extend_highest_gen
+begin
+
+(*
+ lemma red_moment:
+ "extend_highest_gen s th prio tm (moment i t)"
+ apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])
+ apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)
+ by (unfold highest_gen_def, auto dest:step_back_vt_app)
+*)
+
+ lemma ind [consumes 0, case_names Nil Cons, induct type]:
assumes
h0: "R []"
and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e;
@@ -164,237 +154,195 @@
qed
qed
+
lemma th_kept: "th \<in> threads (t @ s) \<and>
- preced th (t@s) = preced th s" (is "?Q t")
+ preced th (t@s) = preced th s" (is "?Q t")
proof -
show ?thesis
proof(induct rule:ind)
case Nil
from threads_s
- show "th \<in> threads ([] @ s) \<and> preced th ([] @ s) = preced th s"
+ show ?case
by auto
next
case (Cons e t)
+ interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
+ interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto
show ?case
proof(cases e)
case (Create thread prio)
- assume eq_e: " e = Create thread prio"
show ?thesis
proof -
- from Cons and eq_e have "step (t@s) (Create thread prio)" by auto
+ from Cons and Create have "step (t@s) (Create thread prio)" by auto
hence "th \<noteq> thread"
proof(cases)
- assume "thread \<notin> threads (t @ s)"
+ case thread_create
with Cons show ?thesis by auto
qed
hence "preced th ((e # t) @ s) = preced th (t @ s)"
- by (unfold eq_e, auto simp:preced_def)
+ by (unfold Create, auto simp:preced_def)
moreover note Cons
ultimately show ?thesis
- by (auto simp:eq_e)
+ by (auto simp:Create)
qed
next
case (Exit thread)
- assume eq_e: "e = Exit thread"
- from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
- from extend_highest_gen.exit_diff [OF this] and eq_e
+ from h_e.exit_diff and Exit
have neq_th: "thread \<noteq> th" by auto
with Cons
show ?thesis
- by (unfold eq_e, auto simp:preced_def)
+ by (unfold Exit, auto simp:preced_def)
next
case (P thread cs)
- assume eq_e: "e = P thread cs"
with Cons
show ?thesis
- by (auto simp:eq_e preced_def)
+ by (auto simp:P preced_def)
next
case (V thread cs)
- assume eq_e: "e = V thread cs"
with Cons
show ?thesis
- by (auto simp:eq_e preced_def)
+ by (auto simp:V preced_def)
next
case (Set thread prio')
- assume eq_e: " e = Set thread prio'"
show ?thesis
proof -
- from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
- from extend_highest_gen.set_diff_low[OF this] and eq_e
+ from h_e.set_diff_low and Set
have "th \<noteq> thread" by auto
hence "preced th ((e # t) @ s) = preced th (t @ s)"
- by (unfold eq_e, auto simp:preced_def)
+ by (unfold Set, auto simp:preced_def)
moreover note Cons
ultimately show ?thesis
- by (auto simp:eq_e)
+ by (auto simp:Set)
qed
qed
qed
qed
-lemma max_kept: "Max ((\<lambda> th'. preced th' (t @ s)) ` (threads (t@s))) = preced th s"
+lemma Max_remove_less:
+ assumes "finite A"
+ and "a \<in> A"
+ and "b \<in> A"
+ and "a \<noteq> b"
+ and "inj_on f A"
+ and "f a = Max (f ` A)"
+ shows "Max (f ` (A - {b})) = (Max (f ` A))"
+proof -
+ have "Max (f ` (A - {b})) = Max (f`A - {f b})"
+ proof -
+ have "f ` (A - {b}) = f ` A - f ` {b}"
+ by (rule inj_on_image_set_diff[OF assms(5)], insert assms(3), auto)
+ thus ?thesis by simp
+ qed
+ also have "... =
+ (if f ` A - {f b} - {f a} = {} then f a else max (f a) (Max (f ` A - {f b} - {f a})))"
+ proof(subst Max.remove)
+ from assms show "f a \<in> f ` A - {f b}"
+ by (meson DiffI empty_iff imageI inj_on_eq_iff insert_iff)
+ next
+ from assms(1) show "finite (f ` A - {f b})" by auto
+ qed auto
+ also have "... = Max (f ` A)" (is "?L = ?R")
+ proof(cases "f ` A - {f b} - {f a} = {}")
+ case True
+ with assms show ?thesis by auto
+ next
+ case False
+ hence "?L = max (f a) (Max (f ` A - {f b} - {f a}))"
+ by simp
+ also have "... = ?R"
+ proof -
+ from assms False
+ have "(Max (f ` A - {f b} - {f a})) \<le> f a" by auto
+ thus ?thesis by (simp add: assms(6) max_def)
+ qed
+ finally show ?thesis .
+ qed
+ finally show ?thesis .
+qed
+
+lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"
proof(induct rule:ind)
case Nil
from highest_preced_thread
- show "Max ((\<lambda>th'. preced th' ([] @ s)) ` threads ([] @ s)) = preced th s"
- by simp
+ show ?case
+ by (unfold the_preced_def, simp)
next
case (Cons e t)
+ interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto
+ interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto
show ?case
proof(cases e)
case (Create thread prio')
- assume eq_e: " e = Create thread prio'"
- from Cons and eq_e have stp: "step (t@s) (Create thread prio')" by auto
- hence neq_thread: "thread \<noteq> th"
- proof(cases)
- assume "thread \<notin> threads (t @ s)"
- moreover have "th \<in> threads (t@s)"
- proof -
- from Cons have "extend_highest_gen s th prio tm t" by auto
- from extend_highest_gen.th_kept[OF this] show ?thesis by (simp)
- qed
- ultimately show ?thesis by auto
- qed
- from Cons have "extend_highest_gen s th prio tm t" by auto
- from extend_highest_gen.th_kept[OF this]
- have h': " th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s"
- by (auto)
- from stp
- have thread_ts: "thread \<notin> threads (t @ s)"
- by (cases, auto)
+ from Cons(2)[unfolded this]
+ have thread_not_in: "thread \<notin> threads (t@s)" by (cases, simp)
show ?thesis (is "Max (?f ` ?A) = ?t")
proof -
- have "Max (?f ` ?A) = Max(insert (?f thread) (?f ` (threads (t@s))))"
- by (unfold eq_e, simp)
+ have "Max (?f ` ?A) = Max (insert (?f thread) (?f ` (threads (t@s))))"
+ by (unfold Create, simp)
moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))"
- proof(rule Max_insert)
- from Cons have "vt (t @ s)" by auto
- from finite_threads[OF this]
+ proof(rule Max.insert)
+ from finite_threads[OF Cons(1)]
show "finite (?f ` (threads (t@s)))" by simp
- next
- from h' show "(?f ` (threads (t@s))) \<noteq> {}" by auto
- qed
- moreover have "(Max (?f ` (threads (t@s)))) = ?t"
+ qed (insert h_t.th_kept, auto)
+ moreover have "(Max (?f ` (threads (t@s)))) = ?t"
proof -
have "(\<lambda>th'. preced th' ((e # t) @ s)) ` threads (t @ s) =
- (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)" (is "?f1 ` ?B = ?f2 ` ?B")
- proof -
- { fix th'
- assume "th' \<in> ?B"
- with thread_ts eq_e
- have "?f1 th' = ?f2 th'" by (auto simp:preced_def)
- } thus ?thesis
- apply (auto simp:Image_def)
- proof -
- fix th'
- assume h: "\<And>th'. th' \<in> threads (t @ s) \<Longrightarrow>
- preced th' (e # t @ s) = preced th' (t @ s)"
- and h1: "th' \<in> threads (t @ s)"
- show "preced th' (t @ s) \<in> (\<lambda>th'. preced th' (e # t @ s)) ` threads (t @ s)"
- proof -
- from h1 have "?f1 th' \<in> ?f1 ` ?B" by auto
- moreover from h[OF h1] have "?f1 th' = ?f2 th'" by simp
- ultimately show ?thesis by simp
- qed
- qed
- qed
- with Cons show ?thesis by auto
+ (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)"
+ by (intro f_image_eq, insert thread_not_in, auto simp:Create preced_def)
+ with Cons show ?thesis by (auto simp:the_preced_def)
qed
moreover have "?f thread < ?t"
proof -
- from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
- from extend_highest_gen.create_low[OF this] and eq_e
+ from h_e.create_low and Create
have "prio' \<le> prio" by auto
thus ?thesis
- by (unfold preced_th, unfold eq_e, insert lt_tm,
- auto simp:preced_def precedence_less_def preced_th)
+ by (unfold preced_th, unfold Create, insert lt_tm,
+ auto simp:preced_def precedence_less_def preced_th the_preced_def)
+ qed
+ ultimately show ?thesis by (auto simp:max_def)
qed
- ultimately show ?thesis by (auto simp:max_def)
- qed
-next
+ next
case (Exit thread)
- assume eq_e: "e = Exit thread"
- from Cons have vt_e: "vt (e#(t @ s))" by auto
- from Cons and eq_e have stp: "step (t@s) (Exit thread)" by auto
- from stp have thread_ts: "thread \<in> threads (t @ s)"
- by(cases, unfold runing_def readys_def, auto)
- from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
- from extend_highest_gen.exit_diff[OF this] and eq_e
- have neq_thread: "thread \<noteq> th" by auto
- from Cons have "extend_highest_gen s th prio tm t" by auto
- from extend_highest_gen.th_kept[OF this]
- have h': "th \<in> threads (t @ s) \<and> preced th (t @ s) = preced th s" .
- show ?thesis (is "Max (?f ` ?A) = ?t")
+ show ?thesis
proof -
- have "threads (t@s) = insert thread ?A"
- by (insert stp thread_ts, unfold eq_e, auto)
- hence "Max (?f ` (threads (t@s))) = Max (?f ` \<dots>)" by simp
- also from this have "\<dots> = Max (insert (?f thread) (?f ` ?A))" by simp
- also have "\<dots> = max (?f thread) (Max (?f ` ?A))"
- proof(rule Max_insert)
- from finite_threads [OF vt_e]
- show "finite (?f ` ?A)" by simp
+ have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) =
+ Max (the_preced (t @ s) ` (threads (t @ s)))"
+ proof(rule Max_remove_less)
+ show "th \<noteq> thread" using Exit h_e.exit_diff by auto
+ next
+ from Cons(2)[unfolded Exit]
+ show "thread \<in> threads (t @ s)"
+ by (cases, simp add: readys_def runing_def)
next
- from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
- from extend_highest_gen.th_kept[OF this]
- show "?f ` ?A \<noteq> {}" by auto
- qed
- finally have "Max (?f ` (threads (t@s))) = max (?f thread) (Max (?f ` ?A))" .
- moreover have "Max (?f ` (threads (t@s))) = ?t"
- proof -
- from Cons show ?thesis
- by (unfold eq_e, auto simp:preced_def)
+ show "finite (threads (t @ s))" by (simp add: finite_threads h_t.vt_t)
+ next
+ show "th \<in> threads (t @ s)" by (simp add: h_t.th_kept)
+ next
+ show "inj_on (the_preced (t @ s)) (threads (t @ s))" by (simp add: inj_the_preced)
+ next
+ show "the_preced (t @ s) th = Max (the_preced (t @ s) ` threads (t @ s))"
+ by (simp add: Cons.hyps(5) h_t.th_kept the_preced_def)
qed
- ultimately have "max (?f thread) (Max (?f ` ?A)) = ?t" by simp
- moreover have "?f thread < ?t"
- proof(unfold eq_e, simp add:preced_def, fold preced_def)
- show "preced thread (t @ s) < ?t"
- proof -
- have "preced thread (t @ s) \<le> ?t"
- proof -
- from Cons
- have "?t = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"
- (is "?t = Max (?g ` ?B)") by simp
- moreover have "?g thread \<le> \<dots>"
- proof(rule Max_ge)
- have "vt (t@s)" by fact
- from finite_threads [OF this]
- show "finite (?g ` ?B)" by simp
- next
- from thread_ts
- show "?g thread \<in> (?g ` ?B)" by auto
- qed
- ultimately show ?thesis by auto
- qed
- moreover have "preced thread (t @ s) \<noteq> ?t"
- proof
- assume "preced thread (t @ s) = preced th s"
- with h' have "preced thread (t @ s) = preced th (t@s)" by simp
- from preced_unique [OF this] have "thread = th"
- proof
- from h' show "th \<in> threads (t @ s)" by simp
- next
- from thread_ts show "thread \<in> threads (t @ s)" .
- qed(simp)
- with neq_thread show "False" by simp
- qed
- ultimately show ?thesis by auto
- qed
- qed
- ultimately show ?thesis
- by (auto simp:max_def split:if_splits)
+ from this[unfolded Cons(5)]
+ have "Max (the_preced (t @ s) ` (threads (t @ s) - {thread})) = preced th s" .
+ moreover have "the_preced ((e # t) @ s) = the_preced (t@s)"
+ by (auto simp:Exit the_preced_def preced_def)
+ ultimately show ?thesis by (simp add:Exit)
qed
next
case (P thread cs)
with Cons
- show ?thesis by (auto simp:preced_def)
+ show ?thesis by (auto simp:preced_def the_preced_def)
next
case (V thread cs)
with Cons
- show ?thesis by (auto simp:preced_def)
- next
+ show ?thesis by (auto simp:preced_def the_preced_def)
+ next (* ccc *)
case (Set thread prio')
- show ?thesis (is "Max (?f ` ?A) = ?t")
+ show ?thesis
+ apply (unfold Set, simp, insert Cons(5)) (* ccc *)
+ find_theorems priority Set
+ find_theorems preced Set
proof -
let ?B = "threads (t@s)"
from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
@@ -964,8 +912,6 @@
apply(auto simp add: detached_eq[OF vt_s])
done
-
-
lemma live: "runing (t@s) \<noteq> {}"
proof(cases "th \<in> runing (t@s)")
case True thus ?thesis by auto