--- a/Correctness.thy Fri Apr 15 14:44:09 2016 +0100
+++ b/Correctness.thy Thu Jun 02 13:15:03 2016 +0100
@@ -52,6 +52,13 @@
sublocale highest_gen < vat_s?: valid_trace "s"
by (unfold_locales, insert vt_s, simp)
+fun occs where
+ "occs Q [] = (if Q [] then 1 else 0::nat)" |
+ "occs Q (x#xs) = (if Q (x#xs) then (1 + occs Q xs) else occs Q xs)"
+
+lemma occs_le: "occs Q t + occs (\<lambda> e. \<not> Q e) t \<le> (1 + length t)"
+ by (induct t, auto)
+
context highest_gen
begin
@@ -68,6 +75,7 @@
@{text "th"} and @{text th} is among these threads,
its @{term cp} must equal to its precedence:
*}
+
lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")
proof -
have "?L \<le> ?R"
@@ -742,6 +750,9 @@
-- {* 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")
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)"
@@ -762,9 +773,82 @@
thus ?thesis using max_preced the_preced_def by auto
qed
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 .
+ qed
+ -- {* Now, since @{term th'} holds the highest @{term cp}
+ and we have already show it is in @{term readys},
+ it is @{term runing} by definition. *}
+ with `th' \<in> readys (t@s)` show ?thesis by (simp add: runing_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)
+ ultimately show ?thesis using that by metis
+qed
+
+lemma (* new proof of th_blockedE *)
+ assumes "th \<notin> runing (t@s)"
+ obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
+ "th' \<in> runing (t@s)"
+proof -
+ -- {* According to @{thm vat_t.th_chain_to_ready}, 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
+ -- {* However, @{term th} can not be in @{term readys}, because otherwise, since
+ @{term th} holds the highest @{term cp}-value, it must be @{term "runing"}. *}
+ moreover have "th \<notin> readys (t@s)"
+ using assms runing_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
+ -- {* We are going to show that this @{term th'} is running. *}
+ have "th' \<in> runing (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")
+ 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) ` (the_thread ` subtree (tRAG (t @ s)) (Th th')))"
+ proof -
+ have "(the_preced (t @ s) \<circ> the_thread) ` subtree (tRAG (t @ s)) (Th th') =
+ the_preced (t @ s) ` the_thread ` subtree (tRAG (t @ s)) (Th th')"
+ by fastforce
+ thus ?thesis by (unfold cp_alt_def1, simp)
+ qed
+ also have "... = (the_preced (t @ s) th)"
+ proof(rule image_Max_subset)
+ show "finite (threads (t@s))" by (simp add: vat_t.finite_threads)
+ next
+ show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)"
+ by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in
+ the_thread.simps vat_t.subtree_tRAG_thread)
+ next
+ show "th \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')"
+ proof -
+ have "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp
+ by (unfold tRAG_subtree_eq, auto simp:subtree_def)
+ thus ?thesis by force
+ qed
+ next
+ show "Max (the_preced (t @ s) ` threads (t @ s)) = the_preced (t @ s) th"
+ by simp
+ qed
+ 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 .
qed
-- {* Now, since @{term th'} holds the highest @{term cp}
@@ -792,5 +876,588 @@
thus ?thesis using th_blockedE by auto
qed
+lemma blockedE:
+ assumes "th \<notin> runing (t@s)"
+ obtains th' where "Th th' \<in> ancestors (RAG (t @ s)) (Th th)"
+ "th' \<in> runing (t@s)"
+ "th' \<in> threads s"
+ "\<not>detached s th'"
+ "cp (t@s) th' = preced th s"
+ "th' \<noteq> th"
+by (metis assms runing_inversion(2) runing_preced_inversion runing_threads_inv th_blockedE)
+
+lemma detached_not_runing:
+ assumes "detached (t@s) th'"
+ and "th' \<noteq> th"
+ shows "th' \<notin> runing (t@s)"
+proof
+ assume otherwise: "th' \<in> runing (t @ s)"
+ have "cp (t@s) th' = cp (t@s) th"
+ proof -
+ have "cp (t@s) th' = Max (cp (t@s) ` readys (t@s))" using otherwise
+ by (simp add:runing_def)
+ moreover have "cp (t@s) th = ..." by (simp add: vat_t.max_cp_readys_threads)
+ ultimately show ?thesis by simp
+ qed
+ moreover have "cp (t@s) th' = preced th' (t@s)" using assms(1)
+ by (simp add: detached_cp_preced)
+ moreover have "cp (t@s) th = preced th (t@s)" by simp
+ ultimately have "preced th' (t@s) = preced th (t@s)" by simp
+ from preced_unique[OF this]
+ have "th' \<in> threads (t @ s) \<Longrightarrow> th \<in> threads (t @ s) \<Longrightarrow> th' = th" .
+ moreover have "th' \<in> threads (t@s)"
+ using otherwise by (unfold runing_def readys_def, auto)
+ moreover have "th \<in> threads (t@s)" by (simp add: th_kept)
+ ultimately have "th' = th" by metis
+ with assms(2) show False by simp
+qed
+
+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.
+
+ 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.
+
+ 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
+ might block @{term th} in @{term t}:
+*}
+
+definition "blockers = {th'. \<not>detached s th' \<and> th' \<noteq> th}"
+
+text {*
+ The following lemma shows that the definition of @{term "blockers"} is correct,
+ i.e. blockers do block @{term "th"}. It is a very simple corollary of @{thm blockedE}.
+*}
+lemma runingE:
+ assumes "th' \<in> runing (t@s)"
+ obtains (is_th) "th' = th"
+ | (is_other) "th' \<in> blockers"
+ using assms blockers_def runing_inversion(2) by auto
+
+text {*
+ The following lemma shows that the number of blockers are finite.
+ The reason is simple, because blockers are subset of thread set, which
+ has been shown finite.
+*}
+
+lemma finite_blockers: "finite blockers"
+proof -
+ have "finite {th'. \<not>detached s th'}"
+ proof -
+ have "finite {th'. Th th' \<in> Field (RAG s)}"
+ proof -
+ have "{th'. Th th' \<in> Field (RAG s)} \<subseteq> threads s"
+ proof
+ fix x
+ assume "x \<in> {th'. Th th' \<in> Field (RAG s)}"
+ thus "x \<in> threads s" using vat_s.RAG_threads by auto
+ qed
+ moreover have "finite ..." by (simp add: vat_s.finite_threads)
+ ultimately show ?thesis using rev_finite_subset by auto
+ qed
+ thus ?thesis by (unfold detached_test, auto)
+ qed
+ thus ?thesis unfolding blockers_def by simp
+qed
+
+text {*
+ The following lemma shows that a blocker may never die
+ as long as the highest thread @{term th} is living.
+
+ The reason for this is that, before a thread can execute an @{term Exit} operation,
+ it must give up all its resource. However, the high priority inherited by a blocker
+ thread also goes with the resources it once held, and the consequence is the lost of
+ right to run, the other precondition for it to execute its own @{term Exit} operation.
+ For this reason, a blocker may never exit before the exit of the highest thread @{term th}.
+*}
+
+lemma blockers_kept:
+ assumes "th' \<in> blockers"
+ shows "th' \<in> threads (t@s)"
+proof(induct rule:ind)
+ case Nil
+ from assms[unfolded blockers_def detached_test]
+ have "Th th' \<in> Field (RAG s)" by simp
+ from vat_s.RAG_threads[OF this]
+ show ?case by simp
+next
+ case h: (Cons e t)
+ interpret et: extend_highest_gen s th prio tm t
+ using h by simp
+ show ?case
+ proof -
+ { assume otherwise: "th' \<notin> threads ((e # t) @ s)"
+ from threads_Exit[OF h(5)] this have eq_e: "e = Exit th'" by auto
+ from h(2)[unfolded this]
+ have False
+ proof(cases)
+ case h: (thread_exit)
+ hence "th' \<in> readys (t@s)" by (auto simp:runing_def)
+ from readys_holdents_detached[OF this h(2)]
+ have "detached (t @ s) th'" .
+ from et.detached_not_runing[OF this] assms[unfolded blockers_def]
+ have "th' \<notin> runing (t @ s)" by auto
+ with h(1) show ?thesis by simp
+ qed
+ } thus ?thesis by auto
+ qed
+qed
+
+text {*
+ The following lemma shows that a blocker may never execute its @{term Create}-operation
+ during the period of @{term t}. The reason is that for a thread to be created
+ (or executing its @{term Create} operation), it must be non-existing (or dead).
+ However, since lemma @{thm blockers_kept} shows that blockers are always living,
+ it can not be created.
+
+ A thread is created only when there is some external reason, there is need for it to run.
+ The precondition for this is that it has already died (or get out of existence).
+*}
+
+lemma blockers_no_create:
+ assumes "th' \<in> blockers"
+ and "e \<in> set t"
+ and "actor e = th'"
+ shows "\<not> isCreate e"
+ using assms(2,3)
+proof(induct rule:ind)
+ case h: (Cons e' t)
+ interpret et: extend_highest_gen s th prio tm t
+ using h by simp
+ { assume eq_e: "e = e'"
+ from et.blockers_kept assms
+ have "th' \<in> threads (t @ s)" by auto
+ with h(2,7)
+ have ?case
+ by (unfold eq_e, cases, auto simp:blockers_def)
+ } with h
+ show ?case by auto
+qed auto
+
+text {*
+ The following lemma shows that, same as blockers,
+ the highest thread @{term th} also can not execute its @{term Create}-operation.
+ And the reason is similar: since @{thm th_kept} says that thread @{term th} is kept live
+ during @{term t}, it can not (or need not) be created another time.
+*}
+lemma th_no_create:
+ assumes "e \<in> set t"
+ and "actor e = th"
+ shows "\<not> isCreate e"
+ using assms
+proof(induct rule:ind)
+ case h:(Cons e' t)
+ interpret et: extend_highest_gen s th prio tm t
+ using h by simp
+ { assume eq_e: "e = e'"
+ from et.th_kept have "th \<in> threads (t @ s)" by simp
+ with h(2,7)
+ have ?case by (unfold eq_e, cases, auto)
+ } with h
+ show ?case by auto
+qed auto
+
+text {*
+ The following is a preliminary lemma in order to show that the number of
+ actions (or operations) taken by the highest thread @{term th} is
+ less or equal to the number of occurrences when @{term th} is in running
+ state. What is proved in this lemma is essentially a strengthening, which
+ says the inequality holds even if the occurrence at the very beginning is
+ ignored.
+
+ The reason for this lemma is that for every operation to be executed, its actor must
+ be in running state. Therefore, there is one occurrence of running state
+ behind every action.
+
+ However, this property does not hold in general, because, for
+ the execution of @{term Create}-operation, the actor does not have to be in running state.
+ Actually, the actor must be in dead state, in order to be created. For @{term th}, this
+ property holds because, according to lemma @{thm th_no_create}, @{term th} can not execute
+ any @{term Create}-operation during the period of @{term t}.
+*}
+lemma actions_th_occs_pre:
+ assumes "t = e'#t'"
+ shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t'"
+ using assms
+proof(induct arbitrary: e' t' rule:ind)
+ case h: (Cons e t e' t')
+ interpret vt: valid_trace "(t@s)" using h(1)
+ by (unfold_locales, simp)
+ interpret ve: extend_highest_gen s th prio tm t using h by simp
+ interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp
+ show ?case (is "?L \<le> ?R")
+ proof(cases t)
+ case Nil
+ show ?thesis
+ proof(cases "actor e = th")
+ case True
+ from ve'.th_no_create[OF _ this]
+ have "\<not> isCreate e" by auto
+ from PIP_actorE[OF h(2) True this] Nil
+ have "th \<in> runing s" by simp
+ hence "?R = 1" using Nil h by simp
+ moreover have "?L = 1" using True Nil by (simp add:actions_of_def)
+ ultimately show ?thesis by simp
+ next
+ case False
+ with Nil
+ show ?thesis by (auto simp:actions_of_def)
+ qed
+ next
+ case h1: (Cons e1 t1)
+ hence eq_t': "t' = e1#t1" using h by simp
+ from h(5)[OF h1]
+ have le: "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t1"
+ (is "?F t \<le> ?G t1") .
+ show ?thesis
+ proof(cases "actor e = th")
+ case True
+ from ve'.th_no_create[OF _ this]
+ have "\<not> isCreate e" by auto
+ from PIP_actorE[OF h(2) True this]
+ have "th \<in> runing (t@s)" by simp
+ hence "?R = 1 + ?G t1" by (unfold h1 eq_t', simp)
+ moreover have "?L = 1 + ?F t" using True by (simp add:actions_of_def)
+ ultimately show ?thesis using le by simp
+ next
+ case False
+ with le
+ show ?thesis by (unfold h1 eq_t', simp add:actions_of_def)
+ qed
+ qed
+qed auto
+
+text {*
+ The following lemma is a simple corollary of @{thm actions_th_occs_pre}. It is the
+ lemma really needed in later proofs.
+*}
+lemma actions_th_occs:
+ shows "length (actions_of {th} t) \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t"
+proof(cases t)
+ case (Cons e' t')
+ from actions_th_occs_pre[OF this]
+ have "length (actions_of {th} t) \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t'" .
+ moreover have "... \<le> occs (\<lambda>t'. th \<in> runing (t' @ s)) t"
+ by (unfold Cons, auto)
+ ultimately show ?thesis by simp
+qed (auto simp:actions_of_def)
+
+text {*
+ The following lemma splits all the operations in @{term t} into three
+ disjoint sets, namely the operations of @{term th}, the operations of
+ blockers and @{term Create}-operations. These sets are mutually disjoint
+ because: @{term "{th}"} and @{term blockers} are disjoint by definition,
+ and neither @{term th} nor any blocker can execute @{term Create}-operation
+ (according to lemma @{thm th_no_create} and @{thm blockers_no_create}).
+
+ One important caveat noted by this lemma is that:
+ Although according to assumption @{thm create_low}, each thread created in
+ @{term t} has precedence lower than @{term th}, therefore, will get no
+ change to run after creation, therefore, can not acquire any resource
+ to become a blocker, the @{term Create}-operations of such
+ lower threads may still consume overall execution time of duration @{term t}, therefore,
+ may compete for execution time with the most urgent thread @{term th}.
+ For PIP to be correct, the number of such competing operations needs to be
+ bounded somehow.
+*}
+
+lemma actions_split:
+ "length t = length (actions_of {th} t) +
+ length (actions_of blockers t) +
+ length (filter (isCreate) t)"
+proof(induct rule:ind)
+ case h: (Cons e t)
+ interpret ve : extend_highest_gen s th prio tm t using h by simp
+ interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp
+ show ?case (is "?L (e#t) = ?T (e#t) + ?O (e#t) + ?C (e#t)")
+ proof(cases "actor e \<in> runing (t@s)")
+ case True
+ thus ?thesis
+ proof(rule ve.runingE)
+ assume 1: "actor e = th"
+ have "?T (e#t) = 1 + ?T (t)" using 1 by (simp add:actions_of_def)
+ moreover have "?O (e#t) = ?O t"
+ proof -
+ have "actor e \<notin> blockers" using 1
+ by (simp add:actions_of_def blockers_def)
+ thus ?thesis by (simp add:actions_of_def)
+ qed
+ moreover have "?C (e#t) = ?C t"
+ proof -
+ from ve'.th_no_create[OF _ 1]
+ have "\<not> isCreate e" by auto
+ thus ?thesis by (simp add:actions_of_def)
+ qed
+ ultimately show ?thesis using h by simp
+ next
+ assume 2: "actor e \<in> ve'.blockers"
+ have "?T (e#t) = ?T (t)"
+ proof -
+ from 2 have "actor e \<noteq> th" by (auto simp:blockers_def)
+ thus ?thesis by (auto simp:actions_of_def)
+ qed
+ moreover have "?O (e#t) = 1 + ?O(t)" using 2
+ by (auto simp:actions_of_def)
+ moreover have "?C (e#t) = ?C(t)"
+ proof -
+ from ve'.blockers_no_create[OF 2, of e]
+ have "\<not> isCreate e" by auto
+ thus ?thesis by (simp add:actions_of_def)
+ qed
+ ultimately show ?thesis using h by simp
+ qed
+ next
+ case False
+ from h(2)
+ have is_create: "isCreate e"
+ by (cases; insert False, auto)
+ have "?T (e#t) = ?T t"
+ proof -
+ have "actor e \<noteq> th"
+ proof
+ assume "actor e = th"
+ from ve'.th_no_create[OF _ this]
+ have "\<not> isCreate e" by auto
+ with is_create show False by simp
+ qed
+ thus ?thesis by (auto simp:actions_of_def)
+ qed
+ moreover have "?O (e#t) = ?O t"
+ proof -
+ have "actor e \<notin> blockers"
+ proof
+ assume "actor e \<in> blockers"
+ from ve'.blockers_no_create[OF this, of e]
+ have "\<not> isCreate e" by simp
+ with is_create show False by simp
+ qed
+ thus ?thesis by (simp add:actions_of_def)
+ qed
+ moreover have "?C (e#t) = 1 + ?C t" using is_create
+ by (auto simp:actions_of_def)
+ ultimately show ?thesis using h by simp
+ qed
+qed (auto simp:actions_of_def)
+
+text {*
+ By combining several of forging lemmas, this lemma gives a upper bound
+ of the occurrence number when the most urgent thread @{term th} is blocked.
+
+ It says, the occasions when @{term th} is blocked during period @{term t}
+ is no more than the number of @{term Create}-operations and
+ the operations taken by blockers plus one.
+
+ Since the length of @{term t} may extend indefinitely, if @{term t} is full
+ of the above mentioned blocking operations, @{term th} may have not chance to run.
+ And, since @{term t} can extend indefinitely, @{term th} my be blocked indefinitely
+ with the growth of @{term t}. Therefore, this lemma alone does not ensure
+ the correctness of PIP.
+
+*}
+
+theorem bound_priority_inversion:
+ "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le>
+ 1 + (length (actions_of blockers t) + length (filter (isCreate) t))"
+ (is "?L \<le> ?R")
+proof -
+ let ?Q = "(\<lambda> t'. th \<in> runing (t'@s))"
+ from occs_le[of ?Q t]
+ have "?L \<le> (1 + length t) - occs ?Q t" by simp
+ also have "... \<le> ?R"
+ proof -
+ have "length t - (length (actions_of blockers t) + length (filter (isCreate) t))
+ \<le> occs (\<lambda> t'. th \<in> runing (t'@s)) t" (is "?L1 \<le> ?R1")
+ proof -
+ have "?L1 = length (actions_of {th} t)" using actions_split by arith
+ also have "... \<le> ?R1" using actions_th_occs by simp
+ finally show ?thesis .
+ qed
+ thus ?thesis by simp
+ qed
+ finally show ?thesis .
+qed
+
end
+
+text {*
+ As explained before, lemma @{text bound_priority_inversion} alone does not
+ ensure the correctness of PIP. For PIP to be correct, the number of blocking operations
+ (by {\em blocking operation}, we mean the @{term Create}-operations and
+ operations taken by blockers) has to be bounded somehow.
+
+ And the following lemma is for this purpose.
+*}
+
+locale bounded_extend_highest = extend_highest_gen +
+ -- {*
+ To bound operations of blockers, the locale specifies that each blocker
+ releases all resources and becomes detached after a certain number
+ of operations. In the assumption, this number is given by the
+ existential variable @{text span}. Notice that this number is fixed for each
+ blocker regardless of any particular instance of @{term t} in which it operates.
+
+ This assumption is reasonable, because it is a common sense that
+ the total number of operations take by any standalone thread (or process)
+ is only determined by its own input, and should not be affected by
+ the particular environment in which it operates. In this particular case,
+ we regard the @{term t} as the environment of thread @{term th}.
+ *}
+ assumes finite_span:
+ "th' \<in> blockers \<Longrightarrow>
+ (\<exists> span. \<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow>
+ length (actions_of {th'} t') = span \<longrightarrow> detached (t'@s) th')"
+ -- {* The following @{text BC} is bound of @{term Create}-operations *}
+ fixes BC
+ -- {*
+ The following assumption requires the number of @{term Create}-operations is
+ less or equal to @{term BC} regardless of any particular extension of @{term t}.
+
+ Although this assumption might seem doubtful at first sight, it is necessary
+ to ensure the occasions when @{term th} is blocked to be finite. Just consider
+ the extreme case when @{term Create}-operations consume all the time in duration
+ @{term "t"} and leave no space for neither @{term "th"} nor blockers to operate.
+ An investigate of the precondition for @{term Create}-operation in the definition
+ of @{term PIP} may reveal that such extreme cases are well possible, because it
+ is only required the thread to be created be a fresh (or dead one), and there
+ are infinitely many such threads.
+
+ However, if we relax the correctness criterion of PIP, allowing @{term th} to be
+ blocked indefinitely while still attaining a certain portion of @{term t} to complete
+ its task, then this bound @{term BC} can be lifted to function depending on @{term t}
+ where @{text "BC t"} is of a certain proportion of @{term "length t"}.
+ *}
+ assumes finite_create:
+ "\<forall> t'. extend_highest_gen s th prio tm t' \<longrightarrow> length (filter isCreate t') \<le> BC"
+begin
+
+text {*
+ The following lemmas show that the number of @{term Create}-operations is bound by @{term BC}:
+*}
+
+lemma create_bc:
+ shows "length (filter isCreate t) \<le> BC"
+ by (meson extend_highest_gen_axioms finite_create)
+
+text {*
+ The following @{term span}-function gives the upper bound of
+ operations take by each particular blocker.
+*}
+definition "span th' = (SOME span.
+ \<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
+ length (actions_of {th'} t') = span \<longrightarrow> detached (t' @ s) th')"
+
+text {*
+ The following lemmas shows the correctness of @{term span}, i.e.
+ the number of operations of taken by @{term th'} is given by
+ @{term "span th"}.
+
+ The reason for this lemma is that since @{term th'} gives up all resources
+ after @{term "span th'"} operations and becomes detached,
+ its inherited high priority is lost, with which the right to run goes as well.
+*}
+lemma le_span:
+ assumes "th' \<in> blockers"
+ shows "length (actions_of {th'} t) \<le> span th'"
+proof -
+ from finite_span[OF assms(1)] obtain span'
+ where span': "\<forall>t'. extend_highest_gen s th prio tm t' \<longrightarrow>
+ length (actions_of {th'} t') = span' \<longrightarrow> detached (t' @ s) th'" (is "?P span'")
+ by auto
+ have "length (actions_of {th'} t) \<le> (SOME span. ?P span)"
+ proof(rule someI2[where a = span'])
+ fix span
+ assume fs: "?P span"
+ show "length (actions_of {th'} t) \<le> span"
+ proof(induct rule:ind)
+ case h: (Cons e t)
+ interpret ve': extend_highest_gen s th prio tm "e#t" using h by simp
+ show ?case
+ proof(cases "length (actions_of {th'} t) < span")
+ case True
+ thus ?thesis by (simp add:actions_of_def)
+ next
+ case False
+ have "actor e \<noteq> th'"
+ proof
+ assume otherwise: "actor e = th'"
+ from ve'.blockers_no_create [OF assms _ this]
+ have "\<not> isCreate e" by auto
+ from PIP_actorE[OF h(2) otherwise this]
+ have "th' \<in> runing (t @ s)" .
+ moreover have "th' \<notin> runing (t @ s)"
+ proof -
+ from False h(4) h(5) have "length (actions_of {th'} t) = span" by simp
+ from fs[rule_format, OF h(3) this] have "detached (t @ s) th'" .
+ from extend_highest_gen.detached_not_runing[OF h(3) this] assms
+ show ?thesis by (auto simp:blockers_def)
+ qed
+ ultimately show False by simp
+ qed
+ with h show ?thesis by (auto simp:actions_of_def)
+ qed
+ qed (simp add: actions_of_def)
+ next
+ from span'
+ show "?P span'" .
+ qed
+ thus ?thesis by (unfold span_def, auto)
+qed
+
+text {*
+ The following lemma is a corollary of @{thm le_span}, which says
+ the total operations of blockers is bounded by the
+ sum of @{term span}-values of all blockers.
+*}
+lemma len_action_blockers:
+ "length (actions_of blockers t) \<le> (\<Sum> th' \<in> blockers . span th')"
+ (is "?L \<le> ?R")
+proof -
+ from len_actions_of_sigma[OF finite_blockers]
+ have "?L = (\<Sum>th'\<in>blockers. length (actions_of {th'} t))" by simp
+ also have "... \<le> ?R"
+ by (rule Groups_Big.setsum_mono, insert le_span, auto)
+ finally show ?thesis .
+qed
+
+text {*
+ By combining forgoing lemmas, it is proved that the number of
+ blocked occurrences of the most urgent thread @{term th} is finitely bounded:
+*}
+theorem priority_inversion_is_finite:
+ "occs (\<lambda> t'. th \<notin> runing (t'@s)) t \<le>
+ 1 + ((\<Sum> th' \<in> blockers . span th') + BC)" (is "?L \<le> ?R" is "_ \<le> 1 + (?A + ?B)" )
+proof -
+ from bound_priority_inversion
+ have "?L \<le> 1 + (length (actions_of blockers t) + length (filter isCreate t))"
+ (is "_ \<le> 1 + (?A' + ?B')") .
+ moreover have "?A' \<le> ?A" using len_action_blockers .
+ moreover have "?B' \<le> ?B" using create_bc .
+ ultimately show ?thesis by simp
+qed
+
+text {*
+ The following lemma says the most urgent thread @{term th} will get as many
+ as operations it wishes, provided @{term t} is long enough.
+ Similar result can also be obtained under the slightly weaker assumption where
+ @{term BC} is lifted to a function and @{text "BC t"} is a portion of
+ @{term "length t"}.
+*}
+theorem enough_actions_for_the_highest:
+ "length t - ((\<Sum> th' \<in> blockers . span th') + BC) \<le> length (actions_of {th} t)"
+ using actions_split create_bc len_action_blockers by linarith
+
end
+
+end
--- a/RTree.thy Fri Apr 15 14:44:09 2016 +0100
+++ b/RTree.thy Thu Jun 02 13:15:03 2016 +0100
@@ -1,5 +1,6 @@
theory RTree
imports "~~/src/HOL/Library/Transitive_Closure_Table" Max
+ (* "Lcrules" *)
begin
section {* A theory of relational trees *}
@@ -99,19 +100,7 @@
*}
lemma edges_in_meaning:
"edges_in r x = {(a, b) | a b. (a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x}"
-proof -
- { fix a b
- assume h: "(a, b) \<in> r" "b \<in> subtree r x"
- moreover have "a \<in> subtree r x"
- proof -
- from h(2)[unfolded subtree_def] have "(b, x) \<in> r^*" by simp
- with h(1) have "(a, x) \<in> r^*" by auto
- thus ?thesis by (auto simp:subtree_def)
- qed
- ultimately have "((a, b) \<in> r \<and> a \<in> subtree r x \<and> b \<in> subtree r x)"
- by (auto)
- } thus ?thesis by (auto simp:edges_in_def)
-qed
+ by (auto simp:edges_in_def subtree_def)
text {*
The following lemma shows the meaning of @{term "edges_in"} from the other side,
@@ -131,48 +120,20 @@
begin
lemma finite_children: "finite (children r x)"
-proof(cases "children r x = {}")
- case True
- thus ?thesis by auto
-next
- case False
- then obtain y where "(y, x) \<in> r" by (auto simp:children_def)
- hence "x \<in> Range r" by auto
- from fb[rule_format, OF this]
- show ?thesis .
-qed
+ using fb by (cases "children r x = {}", auto simp:children_def)
end
locale fsubtree = fbranch +
assumes wf: "wf r"
-(* ccc *)
-
subsection {* Auxiliary lemmas *}
lemma index_minimize:
assumes "P (i::nat)"
obtains j where "P j" and "\<forall> k < j. \<not> P k"
-using assms
-proof -
- have "\<exists> j. P j \<and> (\<forall> k < j. \<not> P k)"
using assms
- proof(induct i rule:less_induct)
- case (less t)
- show ?case
- proof(cases "\<forall> j < t. \<not> P j")
- case True
- with less (2) show ?thesis by blast
- next
- case False
- then obtain j where "j < t" "P j" by auto
- from less(1)[OF this]
- show ?thesis .
- qed
- qed
- with that show ?thesis by metis
-qed
+ by (induct i rule:less_induct, auto)
subsection {* Properties of Relational Graphs and Relational Trees *}
@@ -210,7 +171,7 @@
using assms[unfolded rpath_def]
by (induct, auto simp:pred_of_def rpath_def)
-lemma rpathE:
+lemma rpathE [elim]:
assumes "rpath r x xs y"
obtains (base) "y = x" "xs = []"
| (step) z zs where "(x, z) \<in> r" "rpath r z zs y" "xs = z#zs"
@@ -236,8 +197,15 @@
by (auto simp:pred_of_def rpath_def)
qed
+lemma rpath_stepI'[intro, simp]:
+ assumes "rpath r x xs y"
+ and "(y, z) \<in> r"
+ shows "rpath r x (xs@[z]) z"
+ using assms
+ by (induct, auto)
+
text {* Introduction rule for @{text "@"}-path *}
-lemma rpath_appendI [intro]:
+lemma rpath_appendI [intro,simp]:
assumes "rpath r x xs a" and "rpath r a ys y"
shows "rpath r x (xs @ ys) y"
using assms
@@ -245,7 +213,7 @@
text {* Elimination rule for empty path *}
-lemma rpath_cases [cases pred:rpath]:
+lemma rpath_cases [cases pred:rpath,elim]:
assumes "rpath r a1 a2 a3"
obtains (rbase) "a1 = a3" and "a2 = []"
| (rstep) y :: "'a" and ys :: "'a list"
@@ -258,21 +226,6 @@
obtains "y = x"
using assms[unfolded rpath_def] by auto
--- {* This is a auxiliary lemmas used only in the proof of @{text "rpath_nnl_lastE"} *}
-lemma rpath_nnl_last:
- assumes "rtrancl_path r x xs y"
- and "xs \<noteq> []"
- obtains xs' where "xs = xs'@[y]"
-proof -
- from append_butlast_last_id[OF `xs \<noteq> []`, symmetric]
- obtain xs' y' where eq_xs: "xs = (xs' @ y' # [])" by simp
- with assms(1)
- have "rtrancl_path r x ... y" by simp
- hence "y = y'" by (rule rtrancl_path_appendE, auto)
- with eq_xs have "xs = xs'@[y]" by simp
- from that[OF this] show ?thesis .
-qed
-
text {*
Elimination rule for non-empty paths constructed with @{text "#"}.
*}
@@ -287,145 +240,155 @@
Elimination rule for non-empty path, where the destination node
@{text "y"} is shown to be at the end of the path.
*}
-lemma rpath_nnl_lastE:
+lemma rpath_nnl_lastE [elim]:
assumes "rpath r x xs y"
and "xs \<noteq> []"
obtains xs' where "xs = xs'@[y]"
- using assms[unfolded rpath_def]
- by (rule rpath_nnl_last, auto)
+ using assms
+proof(induct)
+ case (rstep x y ys z)
+ thus ?case by (cases ys, auto)
+qed auto
text {* Other elimination rules of @{text "rpath"} *}
-lemma rpath_appendE:
+lemma rpath_appendE [elim]:
assumes "rpath r x (xs @ [a] @ ys) y"
obtains "rpath r x (xs @ [a]) a" and "rpath r a ys y"
using rtrancl_path_appendE[OF assms[unfolded rpath_def, simplified], folded rpath_def]
by auto
-lemma rpath_subE:
+lemma rpath_subE [elim]:
assumes "rpath r x (xs @ [a] @ ys @ [b] @ zs) y"
obtains "rpath r x (xs @ [a]) a" and "rpath r a (ys @ [b]) b" and "rpath r b zs y"
using assms
by (elim rpath_appendE, auto)
text {* Every path has a unique end point. *}
-lemma rpath_dest_eq:
+lemma rpath_dest_eq [simp]:
assumes "rpath r x xs x1"
and "rpath r x xs x2"
shows "x1 = x2"
using assms
by (induct, auto)
+lemma rpath_dest_eq_simp[simp]:
+ assumes "rpath r x xs1 x1"
+ and "rpath r x xs2 x2"
+ and "xs1 = xs2"
+ shows "x1 = x2"
+ using assms
+ by (induct, auto)
+
subsubsection {* Properites of @{text "edges_on"} *}
-lemma edges_on_unfold:
- "edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R")
-proof -
- { fix c d
- assume "(c, d) \<in> ?L"
- then obtain l1 l2 where h: "(a # b # xs) = l1 @ [c, d] @ l2"
- by (auto simp:edges_on_def)
- have "(c, d) \<in> ?R"
- proof(cases "l1")
- case Nil
- with h have "(c, d) = (a, b)" by auto
- thus ?thesis by auto
- next
- case (Cons e es)
- from h[unfolded this] have "b#xs = es@[c, d]@l2" by auto
- thus ?thesis by (auto simp:edges_on_def)
- qed
- } moreover
- { fix c d
- assume "(c, d) \<in> ?R"
- moreover have "(a, b) \<in> ?L"
- proof -
- have "(a # b # xs) = []@[a,b]@xs" by simp
- hence "\<exists> l1 l2. (a # b # xs) = l1@[a,b]@l2" by auto
- thus ?thesis by (unfold edges_on_def, simp)
- qed
- moreover {
- assume "(c, d) \<in> edges_on (b#xs)"
- then obtain l1 l2 where "b#xs = l1@[c, d]@l2" by (unfold edges_on_def, auto)
- hence "a#b#xs = (a#l1)@[c,d]@l2" by simp
- hence "\<exists> l1 l2. (a # b # xs) = l1@[c,d]@l2" by metis
- hence "(c,d) \<in> ?L" by (unfold edges_on_def, simp)
- }
- ultimately have "(c, d) \<in> ?L" by auto
- } ultimately show ?thesis by auto
-qed
-
-lemma edges_on_len:
- assumes "(a,b) \<in> edges_on l"
- shows "length l \<ge> 2"
+lemma edge_on_headI[simp, intro]:
+ assumes "(a, b) = (a', b')"
+ shows "(a, b) \<in> edges_on (a' # b' # xs)"
using assms
by (unfold edges_on_def, auto)
+lemma edges_on_ConsI[intro]:
+ assumes "(a, b) \<in> edges_on xs"
+ shows "(a, b) \<in> edges_on (x#xs)"
+ using assms
+ apply (unfold edges_on_def, auto)
+ by (meson Cons_eq_appendI)
+
+lemma edges_on_appendI1[intro]:
+ assumes "(a, b) \<in> edges_on xs"
+ shows "(a, b) \<in> edges_on (xs'@xs)"
+ using assms
+ apply (unfold edges_on_def, auto simp:append_assoc)
+ by (metis append_assoc)
+
+lemma edges_on_appendI2[intro]:
+ assumes "(a, b) \<in> edges_on xs"
+ shows "(a, b) \<in> edges_on (xs@xs')"
+ using assms
+ apply (unfold edges_on_def, auto)
+ by metis
+
+lemma edges_onE [elim]:
+ assumes "(a, b) \<in> edges_on xs"
+ obtains a' b' xs' where "(a,b) = (a', b')" "xs = a'#b'#xs'"
+ | a' b' xs' where "(a,b) \<noteq> (a', b')" "xs = a'#b'#xs'" "(a,b) \<in> edges_on (b'#xs')"
+proof(cases xs)
+ case Nil
+ with assms show ?thesis
+ by (unfold edges_on_def, auto)
+next
+ case cs1: (Cons a' xsa)
+ show ?thesis
+ proof(cases xsa)
+ case Nil
+ with cs1 and assms show ?thesis
+ by (unfold edges_on_def, auto)
+ next
+ case (Cons b' xsb)
+ show ?thesis
+ proof(cases "(a,b) = (a', b')")
+ case True
+ with cs1 Cons show ?thesis using that by metis
+ next
+ case False
+ from assms[unfolded cs1 Cons edges_on_def]
+ obtain xs1 ys1 where "a' # b' # xsb = xs1 @ [a, b] @ ys1" by auto
+ moreover with False obtain c xsc where "xs1 = Cons c xsc" by (cases xs1, auto)
+ ultimately have h: "b' # xsb = xsc @ [a, b] @ ys1" by auto
+ show ?thesis
+ apply (rule that(2)[OF False], insert cs1 Cons, simp)
+ using h by auto
+ qed
+ qed
+qed
+
+lemma edges_on_nil [simp]:
+ "edges_on [] = {}" by auto
+
+lemma edges_on_single [simp]:
+ "edges_on [a] = {}" by auto
+
+lemma edges_on_unfold [simp]:
+ "edges_on (a # b # xs) = {(a, b)} \<union> edges_on (b # xs)" (is "?L = ?R")
+by (auto)
+
+lemma edges_on_len:
+ assumes "x \<in> edges_on l"
+ shows "2 \<le> length l" using assms by (cases x, auto)
+
text {* Elimination of @{text "edges_on"} for non-empty path *}
-lemma edges_on_consE [elim, cases set:edges_on]:
+lemma edges_on_consE [elim!, cases set:edges_on]:
assumes "(a,b) \<in> edges_on (x#xs)"
obtains (head) xs' where "x = a" and "xs = b#xs'"
| (tail) "(a,b) \<in> edges_on xs"
-proof -
- from assms obtain l1 l2
- where h: "(x#xs) = l1 @ [a,b] @ l2" by (unfold edges_on_def, blast)
- have "(\<exists> xs'. x = a \<and> xs = b#xs') \<or> ((a,b) \<in> edges_on xs)"
- proof(cases "l1")
- case Nil with h
- show ?thesis by auto
- next
- case (Cons e el)
- from h[unfolded this]
- have "xs = el @ [a,b] @ l2" by auto
- thus ?thesis
- by (unfold edges_on_def, auto)
- qed
- thus ?thesis
- proof
- assume "(\<exists>xs'. x = a \<and> xs = b # xs')"
- then obtain xs' where "x = a" "xs = b#xs'" by blast
- from that(1)[OF this] show ?thesis .
- next
- assume "(a, b) \<in> edges_on xs"
- from that(2)[OF this] show ?thesis .
- qed
-qed
+ using assms
+ by auto
+
text {*
Every edges on the path is a graph edges:
*}
-lemma rpath_edges_on:
+
+lemma rpath_edges_on [intro]:
assumes "rpath r x xs y"
- shows "(edges_on (x#xs)) \<subseteq> r"
- using assms
-proof(induct arbitrary:y)
- case (rbase x)
- thus ?case by (unfold edges_on_def, auto)
-next
- case (rstep x y ys z)
- show ?case
- proof -
- { fix a b
- assume "(a, b) \<in> edges_on (x # y # ys)"
- hence "(a, b) \<in> r" by (cases, insert rstep, auto)
- } thus ?thesis by auto
- qed
-qed
+ shows "edges_on (x#xs) \<subseteq> r"
+ using assms
+ by (induct arbitrary:y, auto)
text {* @{text "edges_on"} is mono with respect to @{text "#"}-operation: *}
-lemma edges_on_Cons_mono:
+lemma edges_on_Cons_mono [intro,simp]:
shows "edges_on xs \<subseteq> edges_on (x#xs)"
-proof -
- { fix a b
- assume "(a, b) \<in> edges_on xs"
- then obtain l1 l2 where "xs = l1 @ [a,b] @ l2"
- by (auto simp:edges_on_def)
- hence "x # xs = (x#l1) @ [a, b] @ l2" by auto
- hence "(a, b) \<in> edges_on (x#xs)"
- by (unfold edges_on_def, blast)
- } thus ?thesis by auto
-qed
+ by auto
+
+lemma edges_on_append_mono [intro,simp]:
+ shows "edges_on xs \<subseteq> edges_on (xs'@xs)"
+ by auto
+
+lemma edges_on_append_mono' [intro,simp]:
+ shows "edges_on xs \<subseteq> edges_on (xs@xs')"
+ by auto
text {*
The following rule @{text "rpath_transfer"} is used to show
@@ -437,68 +400,52 @@
then @{text "x#xs"} is also a edge in graph @{text "r2"}:
*}
-lemma rpath_transfer:
+lemma rpath_transfer[intro]:
assumes "rpath r1 x xs y"
and "edges_on (x#xs) \<subseteq> r2"
shows "rpath r2 x xs y"
using assms
-proof(induct)
- case (rstep x y ys z)
- show ?case
- proof(rule rstepI)
- show "(x, y) \<in> r2"
- proof -
- have "(x, y) \<in> edges_on (x # y # ys)"
- by (unfold edges_on_def, auto)
- with rstep(4) show ?thesis by auto
- qed
- next
- show "rpath r2 y ys z"
- using rstep edges_on_Cons_mono[of "y#ys" "x"] by (auto)
- qed
-qed (unfold rpath_def, auto intro!:Transitive_Closure_Table.rtrancl_path.base)
-
-lemma edges_on_rpathI:
+ by (induct, auto)
+
+lemma edges_on_rpathI[intro, simp]:
assumes "edges_on (a#xs@[b]) \<subseteq> r"
shows "rpath r a (xs@[b]) b"
using assms
-proof(induct xs arbitrary: a b)
- case Nil
- moreover have "(a, b) \<in> edges_on (a # [] @ [b])"
- by (unfold edges_on_def, auto)
- ultimately have "(a, b) \<in> r" by auto
- thus ?case by auto
-next
- case (Cons x xs a b)
- from this(2) have "edges_on (x # xs @ [b]) \<subseteq> r" by (simp add:edges_on_unfold)
- from Cons(1)[OF this] have " rpath r x (xs @ [b]) b" .
- moreover from Cons(2) have "(a, x) \<in> r" by (auto simp:edges_on_unfold)
- ultimately show ?case by (auto)
+ by (induct xs arbitrary: a b, auto)
+
+lemma list_nnl_appendE [elim]:
+ assumes "xs \<noteq> []"
+ obtains x xs' where "xs = xs'@[x]"
+ by (insert assms, rule rev_exhaust, fastforce)
+
+lemma edges_on_rpathI' [intro]:
+ assumes "edges_on (a#xs) \<subseteq> r"
+ and "xs \<noteq> []"
+ and "last xs = b"
+ shows "rpath r a xs b"
+proof -
+ obtain xs' where "xs = xs'@[b]"
+ using assms by fastforce
+ with assms show ?thesis by fastforce
qed
text {*
The following lemma extracts the path from @{text "x"} to @{text "y"}
from proposition @{text "(x, y) \<in> r^*"}
*}
-lemma star_rpath:
+
+lemma star_rpath [elim]:
assumes "(x, y) \<in> r^*"
obtains xs where "rpath r x xs y"
-proof -
- have "\<exists> xs. rpath r x xs y"
- proof(unfold rpath_def, rule iffD1[OF rtranclp_eq_rtrancl_path])
- from assms
- show "(pred_of r)\<^sup>*\<^sup>* x y"
- apply (fold pred_of_star)
- by (auto simp:pred_of_def)
- qed
- from that and this show ?thesis by blast
-qed
+ using assms
+ by (induct, auto)
+
text {*
The following lemma uses the path @{text "xs"} from @{text "x"} to @{text "y"}
as a witness to show @{text "(x, y) \<in> r^*"}.
*}
-lemma rpath_star:
+lemma rpath_star [simp]:
assumes "rpath r x xs y"
shows "(x, y) \<in> r^*"
proof -
@@ -507,25 +454,42 @@
thus ?thesis by (simp add: pred_of_star star_2_pstar)
qed
-lemma subtree_transfer:
+declare rpath_star[elim_format]
+
+lemma rpath_transfer' [intro]:
+ assumes "rpath r1 x xs y"
+ and "r1 \<subseteq> r2"
+ shows "rpath r2 x xs y"
+ using assms
+ by (induct, auto)
+
+lemma subtree_transfer[intro]:
assumes "a \<in> subtree r1 a'"
and "r1 \<subseteq> r2"
shows "a \<in> subtree r2 a'"
+ using assms
proof -
- from assms(1)[unfolded subtree_def]
- have "(a, a') \<in> r1^*" by auto
- from star_rpath[OF this]
- obtain xs where rp: "rpath r1 a xs a'" by blast
- hence "rpath r2 a xs a'"
- proof(rule rpath_transfer)
- from rpath_edges_on[OF rp] and assms(2)
- show "edges_on (a # xs) \<subseteq> r2" by simp
+ from assms(1)
+ obtain xs where h1: "rpath r1 a xs a'" by (auto simp:subtree_def)
+ show ?thesis
+ proof -
+ from rpath_star[OF h1]
+ have "(a, a') \<in> r1\<^sup>*" .
+ with assms(2) have "(a, a') \<in> r2\<^sup>*"
+ using rtrancl_mono subsetCE by blast
+ thus ?thesis by (auto simp:subtree_def)
qed
- from rpath_star[OF this]
- show ?thesis by (auto simp:subtree_def)
-qed
+qed
-lemma subtree_rev_transfer:
+text {*
+ @{text "subtree"} is mono with respect to the underlying graph.
+*}
+lemma subtree_mono[intro]:
+ assumes "r1 \<subseteq> r2"
+ shows "subtree r1 x \<subseteq> subtree r2 x"
+ using assms by auto
+
+lemma subtree_rev_transfer[intro]:
assumes "a \<notin> subtree r2 a'"
and "r1 \<subseteq> r2"
shows "a \<notin> subtree r1 a'"
@@ -535,59 +499,37 @@
The following lemmas establishes a relation from paths in @{text "r"}
to @{text "r^+"} relation.
*}
-lemma rpath_plus:
+lemma rpath_plus[simp]:
assumes "rpath r x xs y"
and "xs \<noteq> []"
shows "(x, y) \<in> r^+"
-proof -
- from assms(2) obtain e es where "xs = e#es" by (cases xs, auto)
- from assms(1)[unfolded this]
- show ?thesis
- proof(cases)
- case rstep
- show ?thesis
- proof -
- from rpath_star[OF rstep(2)] have "(e, y) \<in> r\<^sup>*" .
- with rstep(1) show "(x, y) \<in> r^+" by auto
- qed
- qed
-qed
+ using assms
+ by (induct, simp) fastforce
-lemma plus_rpath:
+lemma plus_rpath [elim]:
assumes "(x, y) \<in> r^+"
obtains xs where "rpath r x xs y" and "xs \<noteq> []"
proof -
from assms
- show ?thesis
- proof(cases rule:converse_tranclE[consumes 1])
- case 1
- hence "rpath r x [y] y" by auto
- from that[OF this] show ?thesis by auto
- next
- case (2 z)
- from 2(2) have "(z, y) \<in> r^*" by auto
- from star_rpath[OF this] obtain xs where "rpath r z xs y" by auto
- from rstepI[OF 2(1) this]
- have "rpath r x (z # xs) y" .
- from that[OF this] show ?thesis by auto
- qed
+ have "\<exists> xs. rpath r x xs y \<and> xs \<noteq> []" by (induct; auto)
+ with that show ?thesis by metis
qed
-
+
subsubsection {* Properties of @{text "subtree"} and @{term "ancestors"}*}
-lemma ancestors_subtreeI:
+lemma ancestors_subtreeI [intro, dest]:
assumes "b \<in> ancestors r a"
shows "a \<in> subtree r b"
using assms by (auto simp:subtree_def ancestors_def)
-lemma ancestors_Field:
+lemma ancestors_Field[elim]:
assumes "b \<in> ancestors r a"
obtains "a \<in> Domain r" "b \<in> Range r"
using assms
apply (unfold ancestors_def, simp)
by (metis Domain.DomainI Range.intros trancl_domain trancl_range)
-lemma subtreeE:
+lemma subtreeE [elim]:
assumes "a \<in> subtree r b"
obtains "a = b"
| "a \<noteq> b" and "b \<in> ancestors r a"
@@ -599,7 +541,7 @@
qed
-lemma subtree_Field:
+lemma subtree_Field [simp, iff]:
"subtree r x \<subseteq> Field r \<union> {x}"
proof
fix y
@@ -610,8 +552,8 @@
thus ?thesis by auto
next
case 2
- thus ?thesis apply (auto simp:ancestors_def)
- using Field_def tranclD by fastforce
+ thus ?thesis
+ by (unfold Field_def, fast)
qed
qed
@@ -620,28 +562,7 @@
and "a \<noteq> b"
shows "b \<in> ancestors r a"
using assms
- by (auto elim!:subtreeE)
-
-text {*
- @{text "subtree"} is mono with respect to the underlying graph.
-*}
-lemma subtree_mono:
- assumes "r1 \<subseteq> r2"
- shows "subtree r1 x \<subseteq> subtree r2 x"
-proof
- fix c
- assume "c \<in> subtree r1 x"
- hence "(c, x) \<in> r1^*" by (auto simp:subtree_def)
- from star_rpath[OF this] obtain xs
- where rp:"rpath r1 c xs x" by metis
- hence "rpath r2 c xs x"
- proof(rule rpath_transfer)
- from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r1" .
- with assms show "edges_on (c # xs) \<subseteq> r2" by auto
- qed
- thus "c \<in> subtree r2 x"
- by (rule rpath_star[elim_format], auto simp:subtree_def)
-qed
+ by auto
text {*
The following lemma characterizes the change of sub-tree of @{text "x"}
@@ -651,14 +572,14 @@
@{term "b \<notin> subtree r x"} amounts to saying @{text "(a, b)"}
is outside the sub-tree of @{text "x"}.
*}
-lemma subtree_del_outside: (* ddd *)
+lemma subtree_del_outside [simp,intro]: (* ddd *)
assumes "b \<notin> subtree r x"
- shows "subtree (r - {(a, b)}) x = (subtree r x)"
+ shows "subtree (r - {(a, b)}) x = (subtree r x)" (is "?L = ?R")
proof -
{ fix c
- assume "c \<in> (subtree r x)"
+ assume "c \<in> ?R"
hence "(c, x) \<in> r^*" by (auto simp:subtree_def)
- hence "c \<in> subtree (r - {(a, b)}) x"
+ hence "c \<in> ?L"
proof(rule star_rpath)
fix xs
assume rp: "rpath r c xs x"
@@ -667,7 +588,7 @@
from rp
have "rpath (r - {(a, b)}) c xs x"
proof(rule rpath_transfer)
- from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r" .
+ from rp have "edges_on (c # xs) \<subseteq> r" ..
moreover have "(a, b) \<notin> edges_on (c#xs)"
proof
assume "(a, b) \<in> edges_on (c # xs)"
@@ -676,27 +597,24 @@
then obtain l1' where eq_xs_b: "xs = l1'@[b]@l2" by (cases l1, auto)
from rp[unfolded this]
show False
- proof(rule rpath_appendE)
- assume "rpath r b l2 x"
- thus ?thesis
- by(rule rpath_star[elim_format], insert assms(1), auto simp:subtree_def)
- qed
+ by (rule rpath_appendE, insert assms(1), auto simp:subtree_def)
qed
- ultimately show "edges_on (c # xs) \<subseteq> r - {(a,b)}" by auto
+ ultimately show "edges_on (c # xs) \<subseteq> (r - {(a, b)})"
+ by (auto)
qed
- thus ?thesis by (rule rpath_star[elim_format], auto simp:subtree_def)
+ thus ?thesis by (auto simp:subtree_def)
qed
qed
} moreover {
fix c
- assume "c \<in> subtree (r - {(a, b)}) x"
- moreover have "... \<subseteq> (subtree r x)" by (rule subtree_mono, auto)
- ultimately have "c \<in> (subtree r x)" by auto
+ assume "c \<in> ?L"
+ moreover have "... \<subseteq> (subtree r x)" by auto
+ ultimately have "c \<in> ?R" by auto
} ultimately show ?thesis by auto
qed
(* ddd *)
-lemma subset_del_subtree_outside: (* ddd *)
+lemma subset_del_subtree_outside [simp, intro]: (* ddd *)
assumes "Range r' \<inter> subtree r x = {}"
shows "subtree (r - r') x = (subtree r x)"
proof -
@@ -712,7 +630,7 @@
from rp
have "rpath (r - r') c xs x"
proof(rule rpath_transfer)
- from rpath_edges_on[OF rp] have "edges_on (c # xs) \<subseteq> r" .
+ from rp have "edges_on (c # xs) \<subseteq> r" ..
moreover {
fix a b
assume h: "(a, b) \<in> r'"
@@ -731,7 +649,7 @@
with assms (1) and h show ?thesis by (auto)
qed
qed
- } ultimately show "edges_on (c # xs) \<subseteq> r - r'" by auto
+ } ultimately show "edges_on (c # xs) \<subseteq> (r - r')" by (auto)
qed
thus ?thesis by (rule rpath_star[elim_format], auto simp:subtree_def)
qed
@@ -744,21 +662,22 @@
} ultimately show ?thesis by auto
qed
-lemma subtree_insert_ext:
+lemma subtree_insert_ext [simp, intro]:
assumes "b \<in> subtree r x"
shows "subtree (r \<union> {(a, b)}) x = (subtree r x) \<union> (subtree r a)"
using assms by (auto simp:subtree_def rtrancl_insert)
-lemma subtree_insert_next:
+lemma subtree_insert_next [simp, intro]:
assumes "b \<notin> subtree r x"
shows "subtree (r \<union> {(a, b)}) x = (subtree r x)"
using assms
by (auto simp:subtree_def rtrancl_insert)
-lemma set_add_rootI:
+lemma set_add_rootI[simp, intro]:
assumes "root r a"
and "a \<notin> Domain r1"
shows "root (r \<union> r1) a"
+ using assms
proof -
let ?r = "r \<union> r1"
{ fix a'
@@ -777,7 +696,7 @@
} thus ?thesis by (auto simp:root_def)
qed
-lemma ancestors_mono:
+lemma ancestors_mono [simp]:
assumes "r1 \<subseteq> r2"
shows "ancestors r1 x \<subseteq> ancestors r2 x"
proof
@@ -788,8 +707,9 @@
h: "rpath r1 x xs a" "xs \<noteq> []" .
have "rpath r2 x xs a"
proof(rule rpath_transfer[OF h(1)])
- from rpath_edges_on[OF h(1)] and assms
- show "edges_on (x # xs) \<subseteq> r2" by auto
+ from h(1) have "edges_on (x # xs) \<subseteq> r1" ..
+ also note assms
+ finally show "edges_on (x # xs) \<subseteq> r2" .
qed
from rpath_plus[OF this h(2)]
show "a \<in> ancestors r2 x" by (auto simp:ancestors_def)
@@ -866,7 +786,7 @@
} ultimately show ?thesis by auto
qed
-lemma rootI:
+lemma rootI [intro]:
assumes h: "\<And> x'. x' \<noteq> x \<Longrightarrow> x \<notin> subtree r' x'"
and "r' \<subseteq> r"
shows "root r' x"
@@ -887,7 +807,7 @@
} thus ?thesis by (auto simp:root_def)
qed
-lemma rpath_overlap_oneside: (* ddd *)
+lemma rpath_overlap_oneside [elim]: (* ddd *)
assumes "rpath r x xs1 x1"
and "rpath r x xs2 x2"
and "length xs1 \<le> length xs2"
@@ -916,7 +836,7 @@
-- {* From thesis inequalities, a number of equations concerning @{text "xs1"}
and @{text "xs2"} are derived *}
have eq_take: "take ?idx xs1 = take ?idx xs2"
- using h2[rule_format, OF lt_j] and h1 by auto
+ using h2[rule_format, OF lt_j] and h1 by linarith
have eq_xs1: " xs1 = take ?idx xs1 @ xs1 ! (?idx) # drop (Suc (?idx)) xs1"
using id_take_nth_drop[OF lt_i] .
have eq_xs2: "xs2 = take ?idx xs2 @ xs2 ! (?idx) # drop (Suc (?idx)) xs2"
@@ -950,22 +870,21 @@
ultimately show ?thesis using neq_idx sgv[unfolded single_valued_def] by metis
next
case False
- then obtain e es where eq_es: "take ?idx xs1 = es@[e]"
- using rev_exhaust by blast
+ then obtain e es where eq_es: "take ?idx xs1 = es@[e]" by fast
have "(e, xs1!?idx) \<in> r"
proof -
from eq_xs1[unfolded eq_es]
have "xs1 = es@[e, xs1!?idx]@drop (Suc ?idx) xs1" by simp
hence "(e, xs1!?idx) \<in> edges_on xs1" by (simp add:edges_on_def, metis)
with rpath_edges_on[OF assms(1)] edges_on_Cons_mono[of xs1 x]
- show ?thesis by auto
+ show ?thesis by (auto)
qed moreover have "(e, xs2!?idx) \<in> r"
proof -
from eq_xs2[folded eq_take, unfolded eq_es]
have "xs2 = es@[e, xs2!?idx]@drop (Suc ?idx) xs2" by simp
hence "(e, xs2!?idx) \<in> edges_on xs2" by (simp add:edges_on_def, metis)
with rpath_edges_on[OF assms(2)] edges_on_Cons_mono[of xs2 x]
- show ?thesis by auto
+ show ?thesis by (auto)
qed
ultimately show ?thesis
using sgv[unfolded single_valued_def] neq_idx by metis
@@ -1068,7 +987,7 @@
with acl show ?thesis by (unfold acyclic_def, auto)
next
case False
- then obtain e es where eq_xs1: "xs1 = es@[e]" using rev_exhaust by auto
+ then obtain e es where eq_xs1: "xs1 = es@[e]" by fast
from assms(2)[unfolded less_1 this]
have "rpath r x (es @ [e] @ xs3) y" by simp
thus ?thesis
@@ -1129,7 +1048,7 @@
show ?thesis by metis
next
case False
- then obtain e es where eq_xs1: "xs1 = es@[e]" using rev_exhaust by blast
+ then obtain e es where eq_xs1: "xs1 = es@[e]" by fast
from rp2[unfolded h this]
have "rpath r z (es @ [e] @ xs3) y" by simp
thus ?thesis
@@ -1204,11 +1123,8 @@
-- {* Extract from the reduced graph the path @{text "xs"} from @{text "c"} to @{text "x"}. *}
then obtain xs where rp0: "rpath ?r' c xs x" by (rule star_rpath, auto)
-- {* It is easy to show @{text "xs"} is also a path in the original graph *}
- hence rp1: "rpath r c xs x"
- proof(rule rpath_transfer)
- from rpath_edges_on[OF rp0]
- show "edges_on (c # xs) \<subseteq> r" by auto
- qed
+ hence rp1: "rpath r c xs x" using rpath_edges_on[OF rp0]
+ by auto
-- {* @{text "xs"} is used as the witness to show that @{text "c"}
in the sub-tree of @{text "x"} in the original graph. *}
hence "c \<in> subtree r x"
@@ -1255,7 +1171,7 @@
proof(cases "xs1 = []")
case True
from rp_c[unfolded this] have "rpath r c [] a" .
- hence eq_c: "c = a" by (rule rpath_nilE, simp)
+ hence eq_c: "c = a" by fast
hence "c#xs = a#xs" by simp
from this and eq_xs have "c#xs = a # xs1 @ b # ys" by simp
from this[unfolded True] have "c#xs = []@[a,b]@ys" by simp
@@ -1269,7 +1185,7 @@
qed
-- {* It can also be shown that @{term "(a,b)"} is not on this fictional path. *}
moreover have "(a, b) \<notin> edges_on (c#xs)"
- using rpath_edges_on[OF rp0] by auto
+ using rpath_edges_on[OF rp0] by (auto)
-- {* Contradiction is thus derived. *}
ultimately show False by auto
qed
@@ -1349,7 +1265,7 @@
qed
}
-- {* The equality of sets is derived from the two directions just proved. *}
- ultimately show ?thesis by auto
+ ultimately show ?thesis by blast
qed
lemma set_del_rootI:
@@ -1461,43 +1377,19 @@
} ultimately show ?thesis by auto
qed
+lemma ancestor_children_subtreeI [intro]:
+ "x \<in> ancestors r z \<Longrightarrow> z \<in> \<Union>(subtree r ` children r x)"
+ by (unfold ancestors_def children_def, auto simp:subtree_def dest:tranclD2)
+
+lemma [iff]: "x \<in> subtree r x"
+ by (auto simp:subtree_def)
+
+lemma [intro]: "xa \<in> children r x \<Longrightarrow> z \<in> subtree r xa \<Longrightarrow> z \<in> subtree r x"
+ by (unfold children_def subtree_def, auto)
lemma subtree_children:
- "subtree r x = {x} \<union> (\<Union> (subtree r ` (children r x)))" (is "?L = ?R")
-proof -
- { fix z
- assume "z \<in> ?L"
- hence "z \<in> ?R"
- proof(cases rule:subtreeE[consumes 1])
- case 2
- hence "(z, x) \<in> r^+" by (auto simp:ancestors_def)
- thus ?thesis
- proof(rule tranclE)
- assume "(z, x) \<in> r"
- hence "z \<in> children r x" by (unfold children_def, auto)
- moreover have "z \<in> subtree r z" by (auto simp:subtree_def)
- ultimately show ?thesis by auto
- next
- fix c
- assume h: "(z, c) \<in> r\<^sup>+" "(c, x) \<in> r"
- hence "c \<in> children r x" by (auto simp:children_def)
- moreover from h have "z \<in> subtree r c" by (auto simp:subtree_def)
- ultimately show ?thesis by auto
- qed
- qed auto
- } moreover {
- fix z
- assume h: "z \<in> ?R"
- have "x \<in> subtree r x" by (auto simp:subtree_def)
- moreover {
- assume "z \<in> \<Union>(subtree r ` children r x)"
- then obtain y where "(y, x) \<in> r" "(z, y) \<in> r^*"
- by (auto simp:subtree_def children_def)
- hence "(z, x) \<in> r^*" by auto
- hence "z \<in> ?L" by (auto simp:subtree_def)
- } ultimately have "z \<in> ?L" using h by auto
- } ultimately show ?thesis by auto
-qed
+ "subtree r x = ({x} \<union> (\<Union> (subtree r ` (children r x))))" (is "?L = ?R")
+ by fast
context fsubtree
begin
@@ -1684,7 +1576,7 @@
qed
qed simp
-lemma compose_relpow_2:
+lemma compose_relpow_2 [intro, simp]:
assumes "r1 \<subseteq> r"
and "r2 \<subseteq> r"
shows "r1 O r2 \<subseteq> r ^^ (2::nat)"
@@ -1698,7 +1590,7 @@
} thus ?thesis by (auto simp:numeral_2_eq_2)
qed
-lemma acyclic_compose:
+lemma acyclic_compose [intro, simp]:
assumes "acyclic r"
and "r1 \<subseteq> r"
and "r2 \<subseteq> r"
@@ -1724,7 +1616,7 @@
"children (r1 O r2) x = \<Union> (children r1 ` (children r2 x))"
by (auto simp:children_def)
-lemma fbranch_compose:
+lemma fbranch_compose [intro, simp]:
assumes "fbranch r1"
and "fbranch r2"
shows "fbranch (r1 O r2)"
@@ -1758,7 +1650,7 @@
} thus ?thesis by (unfold fbranch_def, auto)
qed
-lemma finite_fbranchI:
+lemma finite_fbranchI [intro]:
assumes "finite r"
shows "fbranch r"
proof -
@@ -1774,7 +1666,7 @@
} thus ?thesis by (auto simp:fbranch_def)
qed
-lemma subset_fbranchI:
+lemma subset_fbranchI [intro]:
assumes "fbranch r1"
and "r2 \<subseteq> r1"
shows "fbranch r2"
@@ -1792,17 +1684,17 @@
} thus ?thesis by (auto simp:fbranch_def)
qed
-lemma children_subtree:
+lemma children_subtree [simp, intro]:
shows "children r x \<subseteq> subtree r x"
by (auto simp:children_def subtree_def)
-lemma children_union_kept:
+lemma children_union_kept [simp]:
assumes "x \<notin> Range r'"
shows "children (r \<union> r') x = children r x"
using assms
by (auto simp:children_def)
-lemma wf_rbase:
+lemma wf_rbase [elim]:
assumes "wf r"
obtains b where "(b, a) \<in> r^*" "\<forall> c. (c, b) \<notin> r"
proof -
@@ -1828,7 +1720,7 @@
with that show ?thesis by metis
qed
-lemma wf_base:
+lemma wf_base [elim]:
assumes "wf r"
and "a \<in> Range r"
obtains b where "(b, a) \<in> r^+" "\<forall> c. (c, b) \<notin> r"
@@ -1843,4 +1735,21 @@
with h_b(2) and that show ?thesis by metis
qed
+(*
+lcrules crules
+
+declare crules(26,43,44,45,46,47)[rule del]
+*)
+
+
+declare RTree.subtree_transfer[rule del]
+
+declare RTree.subtreeE[rule del]
+
+declare RTree.ancestors_Field[rule del]
+
+declare RTree.star_rpath[rule del]
+
+declare RTree.plus_rpath[rule del]
+
end
\ No newline at end of file