--- a/Correctness.thy Tue Aug 16 11:49:37 2016 +0100
+++ b/Correctness.thy Wed Aug 24 16:13:20 2016 +0200
@@ -727,68 +727,64 @@
is exactly @{term "th'"}.
*}
lemma th_blockedE: (* ddd, the other main lemma to be presented: *)
- assumes "th \<notin> running (t@s)"
- obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> running (t@s)"
+ assumes "th \<notin> running (t @ s)"
+ obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
+ "th' \<in> running (t @ s)"
proof -
- -- {* According to @{thm vat_t.th_chain_to_ready}, either
+ -- {* According to @{thm vat_t.th_chain_to_ready_tG}, either
@{term "th"} is in @{term "readys"} or there is path leading from it to
one thread in @{term "readys"}. *}
- have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (Th th, Th th') \<in> (RAG (t @ s))\<^sup>+)"
- using th_kept vat_t.th_chain_to_ready by auto
+ have "th \<in> readys (t @ s) \<or> (\<exists>th'. th' \<in> readys (t @ s) \<and> (th, th') \<in> (tG (t @ s))\<^sup>+)"
+ using th_kept vat_t.th_chain_to_ready_tG by blast
+
-- {* However, @{term th} can not be in @{term readys}, because otherwise, since
- @{term th} holds the highest @{term cp}-value, it must be @{term "running"}. *}
- moreover have "th \<notin> readys (t@s)"
+ @{term th} holds the highest @{term cp}-value, it would be @{term "running"}. *}
+ moreover have "th \<notin> readys (t @ s)"
using assms running_def th_cp_max vat_t.max_cp_readys_threads by auto
+
-- {* So, there must be a path from @{term th} to another thread @{text "th'"} in
term @{term readys}: *}
- ultimately obtain th' where th'_in: "th' \<in> readys (t@s)"
- and dp: "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+" by auto
+ ultimately obtain th' where th'_in: "th' \<in> readys (t @ s)"
+ and dp: "(th, th') \<in> (tG (t @ s))\<^sup>+" by auto
+
-- {* We are going to show that this @{term th'} is running. *}
- have "th' \<in> running (t@s)"
+ have "th' \<in> running (t @ s)"
proof -
-- {* We only need to show that this @{term th'} holds the highest @{term cp}-value: *}
- have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" (is "?L = ?R")
+ have "cp (t @ s) th' = Max (cp (t @ s) ` readys (t@s))" (is "?L = ?R")
proof -
-- {* First, by the alternative definition of @{term cp} (I mean @{thm cp_alt_def1}),
the @{term cp}-value of @{term th'} is the maximum of
all precedences of all thread nodes in its @{term tRAG}-subtree: *}
- have "?L = Max ((the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th'))"
- by (unfold cp_alt_def1, simp)
- also have "... = (the_preced (t @ s) \<circ> the_thread) (Th th)"
+ have "?L = Max (the_preced (t @ s) ` (subtree (tG (t @ s)) th'))"
+ by (unfold cp_alt_def2, simp)
+ also have "... = (the_preced (t @ s) th)"
proof(rule image_Max_subset)
- show "finite (Th ` (threads (t@s)))" by (simp add: vat_t.finite_threads)
- next
- show "subtree (tRAG (t @ s)) (Th th') \<subseteq> Th ` threads (t @ s)"
- by (metis Range.intros dp trancl_range vat_t.rg_RAG_threads vat_t.subtree_tRAG_thread)
+ show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads)
next
- show "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
- by (unfold tRAG_subtree_eq, auto simp:subtree_def)
+ show "subtree (tG (t @ s)) th' \<subseteq> threads (t @ s)"
+ using readys_def th'_in vat_t.subtree_tG_thread by auto
next
- show "Max ((the_preced (t @ s) \<circ> the_thread) ` Th ` threads (t @ s)) =
- (the_preced (t @ s) \<circ> the_thread) (Th th)" (is "Max ?L = _")
- proof -
- have "?L = the_preced (t @ s) ` threads (t @ s)"
- by (unfold image_comp, rule image_cong, auto)
- thus ?thesis using max_preced the_preced_def by auto
- qed
+ show "th \<in> subtree (tG (t @ s)) th'"
+ by (simp add: dp subtree_def trancl_into_rtrancl)
+ next
+ show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
+ by simp
qed
- thm the_preced_def
also have "... = ?R"
using th_cp_max th_cp_preced th_kept
the_preced_def vat_t.max_cp_readys_threads by auto
- thm th_cp_max th_cp_preced th_kept
- the_preced_def vat_t.max_cp_readys_threads
- finally show ?thesis .
+ finally show "cp (t @ s) th' = Max (cp (t @ s) ` readys (t @ s))" .
qed
- -- {* Now, since @{term th'} holds the highest @{term cp}
- and we have already show it is in @{term readys},
+
+ -- {* Now, since @{term th'} holds the highest @{term cp}-value in readys,
it is @{term running} by definition. *}
- with `th' \<in> readys (t@s)` show ?thesis by (simp add: running_def)
+ with `th' \<in> readys (t @ s)` show "th' \<in> running (t @ s)" by (simp add: running_def)
qed
+
-- {* It is easy to show @{term th'} is an ancestor of @{term th}: *}
- moreover have "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- using `(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+` by (auto simp:ancestors_def)
+ moreover have "th' \<in> ancestors (tG (t @ s)) th"
+ by (simp add: ancestors_def dp)
ultimately show ?thesis using that by metis
qed
@@ -863,18 +859,22 @@
qed
lemma th_blockedE_pretty:
- assumes "th \<notin> running (t@s)"
- shows "\<exists>th'. Th th' \<in> ancestors (RAG (t @ s)) (Th th) \<and> th' \<in> running (t@s)"
-using th_blockedE assms by blast
+ assumes "th \<notin> running (t @ s)"
+ shows "\<exists>th'. th' \<in> ancestors (tG (t @ s)) th \<and> th' \<in> running (t @ s)"
+using th_blockedE assms
+by blast
+
+
+
text {*
Now it is easy to see there is always a thread to run by case analysis
- on whether thread @{term th} is running: if the answer is Yes, the
+ on whether thread @{term th} is running: if the answer is yes, the
the running thread is obviously @{term th} itself; otherwise, the running
thread is the @{text th'} given by lemma @{thm th_blockedE}.
*}
-lemma live: "running (t@s) \<noteq> {}"
-proof(cases "th \<in> running (t@s)")
+lemma live: "running (t @ s) \<noteq> {}"
+proof(cases "th \<in> running (t @ s)")
case True thus ?thesis by auto
next
case False
@@ -882,19 +882,20 @@
qed
lemma blockedE:
- assumes "th \<notin> running (t@s)"
- obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
- "th' \<in> running (t@s)"
+ assumes "th \<notin> running (t @ s)"
+ obtains th' where "th' \<in> ancestors (tG (t @ s)) th"
+ "th' \<in> running (t @ s)"
"th' \<in> threads s"
"\<not>detached s th'"
- "cp (t@s) th' = preced th s"
+ "cp (t @ s) th' = preced th s"
"th' \<noteq> th"
-by (metis assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE)
+using assms running_inversion(2) running_preced_inversion running_threads_inv th_blockedE
+by metis
lemma detached_not_running:
- assumes "detached (t@s) th'"
+ assumes "detached (t @ s) th'"
and "th' \<noteq> th"
- shows "th' \<notin> running (t@s)"
+ shows "th' \<notin> running (t @ s)"
proof
assume otherwise: "th' \<in> running (t @ s)"
have "cp (t@s) th' = cp (t@s) th"
@@ -920,19 +921,21 @@
section {* The correctness theorem of PIP *}
text {*
- In this section, we identify two more conditions in addition to the ones already
- specified in the forgoing locales, based on which the correctness of PIP is
- formally proved.
+
+ In this section, we identify two more conditions in addition to the ones
+ already specified in the current locale, based on which the correctness
+ of PIP is formally proved.
- Note that Priority Inversion refers to the phenomenon where the thread with highest priority
- is blocked by one with lower priority because the resource it is requesting is
- currently held by the later. The objective of PIP is to avoid {\em Indefinite Priority Inversion},
- i.e. the number of occurrences of {\em Prioirty Inversion} becomes indefinitely large.
+ Note that Priority Inversion refers to the phenomenon where the thread
+ with highest priority is blocked by one with lower priority because the
+ resource it is requesting is currently held by the later. The objective of
+ PIP is to avoid {\em Indefinite Priority Inversion}, i.e. the number of
+ occurrences of {\em Priority Inversion} becomes indefinitely large.
- For PIP to be correct, a finite upper bound needs to be found for the occurrence number,
- and the existence. This section makes explicit two more conditions so that the existence
- of such a upper bound can be proved to exist.
-*}
+ For PIP to be correct, a finite upper bound needs to be found for the
+ occurrence number, and the existence. This section makes explicit two more
+ conditions so that the existence of such a upper bound can be proved to
+ exist. *}
text {*
The following set @{text "blockers"} characterizes the set of threads which
--- a/Journal/Paper.thy Tue Aug 16 11:49:37 2016 +0100
+++ b/Journal/Paper.thy Wed Aug 24 16:13:20 2016 +0200
@@ -873,6 +873,55 @@
properties that show our model of PIP is correct.
*}
+section {* Preliminaries *}
+
+(*<*)
+context valid_trace
+begin
+(*>*)
+text {*
+
+ In this section we prove facts that immediately follow from
+ our definitions of valid traces.
+
+ \begin{lemma}??\label{precedunique}
+ @{thm [mode=IfThen] preced_unique[where ?th1.0=th\<^sub>1 and ?th2.0=th\<^sub>2]}
+ \end{lemma}
+
+
+ We can verify that in any valid state, there can only be at most
+ one running thread---if there are more than one running thread,
+ say @{text "th\<^sub>1"} and @{text "th\<^sub>2"}, they must be
+ equal.
+
+ \begin{lemma}
+ @{thm [mode=IfThen] running_unique[where ?th1.0=th\<^sub>1 and ?th2.0=th\<^sub>2]}
+ \end{lemma}
+
+ \begin{proof}
+ Since @{text "th\<^sub>1"} and @{text "th\<^sub>2"} are running, they must be
+ roots in the RAG.
+ According to XXX, there exists a chain in the RAG-subtree of @{text "th\<^sub>1"},
+ say starting from @{text "th'\<^sub>1"}, such that @{text "th'\<^sub>1"} has the
+ highest precedence in this subtree (@{text "th\<^sub>1"} inherited
+ the precedence of @{text "th'\<^sub>1"}). We have a similar chain starting from, say
+ @{text "th'\<^sub>2"}, in the RAG-subtree of @{text "th\<^sub>2"}. Since @{text "th\<^sub>1"}
+ and @{text "th\<^sub>2"} are running we know their cp-value must be the same, that is
+ \begin{center}
+ @{term "cp s th\<^sub>1 = cp s th\<^sub>2"}
+ \end{center}
+
+ \noindent
+ That means the precedences of @{text "th'\<^sub>1"} and @{text "th'\<^sub>2"}
+ must be the same (they are the maxima in the respective RAG-subtrees). From this we can
+ infer by Lemma~\ref{precedunique} that @{text "th'\<^sub>1"}
+ and @{text "th'\<^sub>2"} are the same threads. However, this also means the
+ roots @{text "th\<^sub>1"} and @{text "th\<^sub>2"} must be the same.\qed
+ \end{proof}
+
+ *}
+(*<*)end(*>*)
+
section {* The Correctness Proof *}
(*<*)
--- a/PIPBasics.thy Tue Aug 16 11:49:37 2016 +0100
+++ b/PIPBasics.thy Wed Aug 24 16:13:20 2016 +0200
@@ -920,6 +920,8 @@
"dependants s th = {th'. th \<in> ancestors (tG s) th'}"
by (unfold dependants_alt_tG ancestors_def, simp)
+
+
section {* Locales used to investigate the execution of PIP *}
text {*
@@ -3459,6 +3461,36 @@
qed
qed
+lemma root_readys:
+ assumes "th \<in> readys s"
+ shows "root (tRAG s) (Th th)"
+proof -
+ { assume "\<not> root (tRAG s) (Th th)"
+ then obtain n' where "(Th th, n') \<in> (tRAG s)^+"
+ unfolding root_def ancestors_def by auto
+ then obtain cs where "(Th th, Cs cs) \<in> RAG s"
+ unfolding tRAG_alt_def using tranclD by fastforce
+ then have "th \<notin> readys s"
+ unfolding readys_def using in_RAG_E by blast
+ with assms have False by simp
+ } then show "root (tRAG s) (Th th)" by auto
+qed
+
+lemma root_readys_tG:
+ assumes "th \<in> readys s"
+ shows "root (tG s) th"
+proof -
+ { assume "\<not> root (tG s) th"
+ then obtain th' where "(th, th') \<in> (tG s)^+"
+ unfolding root_def ancestors_def by auto
+ then have "(Th th, Th th') \<in> (tRAG s)^+"
+ using trancl_tG_tRAG by simp
+ with root_readys assms
+ have False
+ unfolding root_def ancestors_def by auto
+ } then show "root (tG s) th" by auto
+qed
+
lemma readys_indep:
assumes "th1 \<in> readys s"
and "th2 \<in> readys s"
@@ -3509,191 +3541,67 @@
The following two lemmas shows there is at most one running thread
in the system.
*}
+
+
lemma running_unique:
assumes running_1: "th1 \<in> running s"
and running_2: "th2 \<in> running s"
shows "th1 = th2"
proof -
- -- {* According to lemma @{thm thread_chain},
- each living threads is chained to a thread in its subtree, and this
- target thread holds the highest precedence of the subtree.
-
- The chains for @{term th1} and @{term th2} are established
- first in the following in @{text "h1"} and @{text "h2"}:
- *}
+ -- {*
+
+ According to lemma @{thm thread_chain}, each live thread is chained to a
+ thread in its subtree, who holds the highest precedence of the subtree.
+
+ The chains for @{term th1} and @{term th2} are established first in the
+ following in @{text "chain1"} and @{text "chain2"}. These chains start
+ with the threads @{text "th1'"} and @{text "th2'"} respectively. *}
+
have "th1 \<in> threads s" using assms
by (unfold running_def readys_def, auto)
- from thread_chain[OF this]
+ with thread_chain
obtain th1' where
- h1: "th1' \<in> subtree (tG s) th1"
+ chain1: "th1' \<in> subtree (tG s) th1"
"the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)"
"th1' \<in> threads s"
by auto
have "th2 \<in> threads s" using assms
by (unfold running_def readys_def, auto)
- from thread_chain[OF this]
+ with thread_chain
obtain th2' where
- h2: "th2' \<in> subtree (tG s) th2"
+ chain2: "th2' \<in> subtree (tG s) th2"
"the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)"
"th2' \<in> threads s"
by auto
- -- {* It can be proved that the chained thread for @{term th1} and @{term th2}
- must be equal:
+ -- {* From these two chains we can be prove that the threads
+ @{term th1} and @{term th2} must be equal. For this we first
+ show that the starting points of the chains are equal.
*}
have eq_th': "th1' = th2'"
proof -
- have "the_preced s th1' = the_preced s th2'"
- proof -
- from running_1 and running_2 have "cp s th1 = cp s th2"
- unfolding running_def by auto
- from this[unfolded cp_alt_def2]
- have eq_max: "Max (the_preced s ` subtree (tG s) th1) =
- Max (the_preced s ` subtree (tG s) th2)" .
- with h1(2) h2(2)
- show ?thesis by metis
- qed
- from preced_unique[OF this[unfolded the_preced_def] h1(3) h2(3)]
- show ?thesis .
- qed
- -- {* From this, it can be derived that the two sub-trees
- rooted by @{term th1} and @{term th2} must overlap: *}
- have overlapping: "th1' \<in> subtree (tG s) th1 \<inter> subtree (tG s) th2"
- using eq_th' h1(1) h2(1) by auto
- -- {* However, this would be in contradiction with the fact
- that two independent sub-trees can not overlap,
- if @{term "th1 \<noteq> th2"} (therefore, each roots an independent sub-trees).
- Therefore, @{term th1} and @{term th2} must be equal.
- *}
- { assume neq: "th1 \<noteq> th2"
- -- {* According to @{thm readys_indep_tG}, two different threads
- in ready queue must be independent with each other: *}
- have "indep (tG s) th1 th2"
- by (rule readys_indep_tG[OF _ _ neq], insert assms, auto simp:running_def)
- -- {* Therefore, according to lemma @{thm subtree_disjoint},
- the two sub-trees rooted by them can not overlap:
- *}
- from subtree_disjoint[OF this]
- have "subtree (tG s) th1 \<inter> subtree (tG s) th2 = {}" .
- -- {* In contradiction with @{thm overlapping}: *}
- with overlapping have False by auto
- } thus ?thesis by auto
-qed
-
-text {*
- The following two lemmas shows there is at most one running thread
- in the system.
-*}
-lemma running_unique_old:
- assumes running_1: "th1 \<in> running s"
- and running_2: "th2 \<in> running s"
- shows "th1 = th2"
-proof -
- from running_1 and running_2 have "cp s th1 = cp s th2"
- unfolding running_def by auto
- from this[unfolded cp_alt_def]
- have eq_max:
- "Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) =
- Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th2)})"
- (is "Max ?L = Max ?R") .
- have "Max ?L \<in> ?L"
- proof(rule Max_in)
- show "finite ?L" by (simp add: finite_subtree_threads)
- next
- show "?L \<noteq> {}" using subtree_def by fastforce
- qed
- then obtain th1' where
- h_1: "Th th1' \<in> subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L"
- by auto
- have "Max ?R \<in> ?R"
- proof(rule Max_in)
- show "finite ?R" by (simp add: finite_subtree_threads)
- next
- show "?R \<noteq> {}" using subtree_def by fastforce
+ -- {* from @{text th1} and @{text th2} running, we know their
+ cp-value is the same *}
+ from running_1 and running_2 have "cp s th1 = cp s th2"
+ unfolding running_def by auto
+ -- {* that means the preced of @{text th1'} and @{text th2'}
+ must be the same *}
+ then
+ have eq_max: "Max (the_preced s ` subtree (tG s) th1) =
+ Max (the_preced s ` subtree (tG s) th2)"
+ unfolding cp_alt_def2 .
+ with chain1(2) chain2(2)
+ have "the_preced s th1' = the_preced s th2'" by simp
+ -- {* since the precedences are the same, we can conclude
+ that @{text th1'} and @{text th2'} are the same *}
+ with preced_unique chain1(3) chain2(3)
+ show "th1' = th2'" unfolding the_preced_def by auto
qed
- then obtain th2' where
- h_2: "Th th2' \<in> subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R"
- by auto
- have "th1' = th2'"
- proof(rule preced_unique)
- from h_1(1)
- show "th1' \<in> threads s"
- proof(cases rule:subtreeE)
- case 1
- hence "th1' = th1" by simp
- with running_1 show ?thesis by (auto simp:running_def readys_def)
- next
- case 2
- from this(2)
- have "(Th th1', Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)
- from tranclD[OF this]
- have "(Th th1') \<in> Domain (RAG s)" by auto
- from dm_RAG_threads[OF this] show ?thesis .
- qed
- next
- from h_2(1)
- show "th2' \<in> threads s"
- proof(cases rule:subtreeE)
- case 1
- hence "th2' = th2" by simp
- with running_2 show ?thesis by (auto simp:running_def readys_def)
- next
- case 2
- from this(2)
- have "(Th th2', Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)
- from tranclD[OF this]
- have "(Th th2') \<in> Domain (RAG s)" by auto
- from dm_RAG_threads[OF this] show ?thesis .
- qed
- next
- have "the_preced s th1' = the_preced s th2'"
- using eq_max h_1(2) h_2(2) by metis
- thus "preced th1' s = preced th2' s" by (simp add:the_preced_def)
- qed
- from h_1(1)[unfolded this]
- have star1: "(Th th2', Th th1) \<in> (RAG s)^*" by (auto simp:subtree_def)
- from h_2(1)[unfolded this]
- have star2: "(Th th2', Th th2) \<in> (RAG s)^*" by (auto simp:subtree_def)
- from star_rpath[OF star1] obtain xs1
- where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)"
- by auto
- from star_rpath[OF star2] obtain xs2
- where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)"
- by auto
- from rp1 rp2
- show ?thesis
- proof(cases)
- case (less_1 xs')
- moreover have "xs' = []"
- proof(rule ccontr)
- assume otherwise: "xs' \<noteq> []"
- from rpath_plus[OF less_1(3) this]
- have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" .
- from tranclD[OF this]
- obtain cs where "waiting s th1 cs"
- by (unfold s_RAG_def, fold s_waiting_abv, auto)
- with running_1 show False
- by (unfold running_def readys_def, auto)
- qed
- ultimately have "xs2 = xs1" by simp
- from rpath_dest_eq[OF rp1 rp2[unfolded this]]
- show ?thesis by simp
- next
- case (less_2 xs')
- moreover have "xs' = []"
- proof(rule ccontr)
- assume otherwise: "xs' \<noteq> []"
- from rpath_plus[OF less_2(3) this]
- have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" .
- from tranclD[OF this]
- obtain cs where "waiting s th2 cs"
- by (unfold s_RAG_def, fold s_waiting_abv, auto)
- with running_2 show False
- by (unfold running_def readys_def, auto)
- qed
- ultimately have "xs2 = xs1" by simp
- from rpath_dest_eq[OF rp1 rp2[unfolded this]]
- show ?thesis by simp
- qed
+ moreover
+ have "root (tG s) th1" "root (tG s) th2" using assms
+ using assms root_readys_tG
+ unfolding running_def by auto
+ ultimately show "th1 = th2" using root_unique chain1(1) chain2(1)
+ by fastforce
qed
lemma card_running:
--- a/RTree.thy Tue Aug 16 11:49:37 2016 +0100
+++ b/RTree.thy Wed Aug 24 16:13:20 2016 +0200
@@ -73,12 +73,28 @@
nodes (including itself) which can reach @{text "x"} by following
some path in @{text "r"}: *}
-definition "subtree r x = {node' . (node', x) \<in> r^*}"
+definition "subtree r x = {y . (y, x) \<in> r^*}"
-definition "ancestors r x = {node'. (x, node') \<in> r^+}"
+definition "ancestors r x = {y. (x, y) \<in> r^+}"
definition "root r x = (ancestors r x = {})"
+lemma root_indep:
+ assumes "root r x"
+ and "root r y"
+ and "y \<noteq> x"
+ shows "indep r x y"
+proof -
+ { assume "(x, y) \<in> r^*"
+ hence False using assms
+ by (unfold root_def ancestors_def, auto dest:tranclD rtranclD)
+ } moreover {
+ assume "(y, x) \<in> r^*"
+ hence False using assms
+ by (unfold root_def ancestors_def, auto dest:tranclD rtranclD)
+ } ultimately show ?thesis by (auto simp:indep_def)
+qed
+
text {*
The following @{text "edge_in r x"} is the set of edges contained in
@@ -108,7 +124,7 @@
shows "(a, b) \<notin> edges_in r x"
using assms by (unfold edges_in_def subtree_def, auto)
-definition "children r x = {node'. (node', x) \<in> r}"
+definition "children r x = {y. (y, x) \<in> r}"
locale fforest = forest +
assumes fb: "finite (children r x)"
@@ -1067,6 +1083,21 @@
} thus ?thesis by auto
qed
+lemma root_unique:
+ assumes "x \<in> subtree r y"
+ and "x \<in> subtree r z"
+ and "root r y"
+ and "root r z"
+ shows "y = z"
+proof -
+ { assume "y \<noteq> z"
+ from root_indep[OF assms(4,3) this]
+ have "indep r z y" .
+ from subtree_disjoint[OF this] and assms
+ have False by auto
+ } thus ?thesis by auto
+qed
+
text {*
The following lemma @{text "subtree_del"} characterizes the change of sub-tree of
@{text "x"} with the removal of an inside edge @{text "(a, b)"}.
Binary file journal.pdf has changed