# HG changeset patch # User Christian Urban # Date 1464869703 -3600 # Node ID 95e7933968f8cfff3bb29e6aee6b0bfae4185afc # Parent 71a3300d497b1ecfc03627f550003dabd87c30c5 updated diff -r 71a3300d497b -r 95e7933968f8 Correctness.thy --- 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 (\ e. \ Q e) t \ (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 \ ?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) \ the_thread) ` subtree (tRAG (t @ s)) (Th th'))" by (unfold cp_alt_def1, simp) also have "... = (the_preced (t @ s) \ 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' \ 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' \ ancestors (RAG (t @ s)) (Th th)" + using `(Th th, Th th') \ (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 \ runing (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ 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 \ readys (t @ s) \ (\th'. th' \ readys (t @ s) \ (Th th, Th th') \ (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 \ 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' \ readys (t@s)" + and dp: "(Th th, Th th') \ (RAG (t @ s))\<^sup>+" by auto + -- {* We are going to show that this @{term th'} is running. *} + have "th' \ 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) \ 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') \ 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 \ the_thread ` subtree (tRAG (t @ s)) (Th th')" + proof - + have "Th th \ 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 \ runing (t@s)" + obtains th' where "Th th' \ ancestors (RAG (t @ s)) (Th th)" + "th' \ runing (t@s)" + "th' \ threads s" + "\detached s th'" + "cp (t@s) th' = preced th s" + "th' \ 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' \ th" + shows "th' \ runing (t@s)" +proof + assume otherwise: "th' \ 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' \ threads (t @ s) \ th \ threads (t @ s) \ th' = th" . + moreover have "th' \ threads (t@s)" + using otherwise by (unfold runing_def readys_def, auto) + moreover have "th \ 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'. \detached s th' \ th' \ 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' \ runing (t@s)" + obtains (is_th) "th' = th" + | (is_other) "th' \ 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'. \detached s th'}" + proof - + have "finite {th'. Th th' \ Field (RAG s)}" + proof - + have "{th'. Th th' \ Field (RAG s)} \ threads s" + proof + fix x + assume "x \ {th'. Th th' \ Field (RAG s)}" + thus "x \ 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' \ blockers" + shows "th' \ threads (t@s)" +proof(induct rule:ind) + case Nil + from assms[unfolded blockers_def detached_test] + have "Th th' \ 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' \ 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' \ 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' \ 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' \ blockers" + and "e \ set t" + and "actor e = th'" + shows "\ 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' \ 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 \ set t" + and "actor e = th" + shows "\ 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 \ 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) \ occs (\ t'. th \ 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 \ ?R") + proof(cases t) + case Nil + show ?thesis + proof(cases "actor e = th") + case True + from ve'.th_no_create[OF _ this] + have "\ isCreate e" by auto + from PIP_actorE[OF h(2) True this] Nil + have "th \ 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) \ occs (\t'. th \ runing (t' @ s)) t1" + (is "?F t \ ?G t1") . + show ?thesis + proof(cases "actor e = th") + case True + from ve'.th_no_create[OF _ this] + have "\ isCreate e" by auto + from PIP_actorE[OF h(2) True this] + have "th \ 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) \ occs (\ t'. th \ runing (t'@s)) t" +proof(cases t) + case (Cons e' t') + from actions_th_occs_pre[OF this] + have "length (actions_of {th} t) \ occs (\t'. th \ runing (t' @ s)) t'" . + moreover have "... \ occs (\t'. th \ 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 \ 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 \ 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 "\ 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 \ ve'.blockers" + have "?T (e#t) = ?T (t)" + proof - + from 2 have "actor e \ 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 "\ 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 \ th" + proof + assume "actor e = th" + from ve'.th_no_create[OF _ this] + have "\ 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 \ blockers" + proof + assume "actor e \ blockers" + from ve'.blockers_no_create[OF this, of e] + have "\ 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 (\ t'. th \ runing (t'@s)) t \ + 1 + (length (actions_of blockers t) + length (filter (isCreate) t))" + (is "?L \ ?R") +proof - + let ?Q = "(\ t'. th \ runing (t'@s))" + from occs_le[of ?Q t] + have "?L \ (1 + length t) - occs ?Q t" by simp + also have "... \ ?R" + proof - + have "length t - (length (actions_of blockers t) + length (filter (isCreate) t)) + \ occs (\ t'. th \ runing (t'@s)) t" (is "?L1 \ ?R1") + proof - + have "?L1 = length (actions_of {th} t)" using actions_split by arith + also have "... \ ?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' \ blockers \ + (\ span. \ t'. extend_highest_gen s th prio tm t' \ + length (actions_of {th'} t') = span \ 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: + "\ t'. extend_highest_gen s th prio tm t' \ length (filter isCreate t') \ 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) \ 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. + \t'. extend_highest_gen s th prio tm t' \ + length (actions_of {th'} t') = span \ 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' \ blockers" + shows "length (actions_of {th'} t) \ span th'" +proof - + from finite_span[OF assms(1)] obtain span' + where span': "\t'. extend_highest_gen s th prio tm t' \ + length (actions_of {th'} t') = span' \ detached (t' @ s) th'" (is "?P span'") + by auto + have "length (actions_of {th'} t) \ (SOME span. ?P span)" + proof(rule someI2[where a = span']) + fix span + assume fs: "?P span" + show "length (actions_of {th'} t) \ 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 \ th'" + proof + assume otherwise: "actor e = th'" + from ve'.blockers_no_create [OF assms _ this] + have "\ isCreate e" by auto + from PIP_actorE[OF h(2) otherwise this] + have "th' \ runing (t @ s)" . + moreover have "th' \ 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) \ (\ th' \ blockers . span th')" + (is "?L \ ?R") +proof - + from len_actions_of_sigma[OF finite_blockers] + have "?L = (\th'\blockers. length (actions_of {th'} t))" by simp + also have "... \ ?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 (\ t'. th \ runing (t'@s)) t \ + 1 + ((\ th' \ blockers . span th') + BC)" (is "?L \ ?R" is "_ \ 1 + (?A + ?B)" ) +proof - + from bound_priority_inversion + have "?L \ 1 + (length (actions_of blockers t) + length (filter isCreate t))" + (is "_ \ 1 + (?A' + ?B')") . + moreover have "?A' \ ?A" using len_action_blockers . + moreover have "?B' \ ?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 - ((\ th' \ blockers . span th') + BC) \ length (actions_of {th} t)" + using actions_split create_bc len_action_blockers by linarith + end + +end diff -r 71a3300d497b -r 95e7933968f8 Journal/Paper.thy --- a/Journal/Paper.thy Fri Apr 15 14:44:09 2016 +0100 +++ b/Journal/Paper.thy Thu Jun 02 13:15:03 2016 +0100 @@ -1002,15 +1002,47 @@ proof, which means the difference between the counters @{const cntV} and @{const cntP} can be larger than @{term 1}. - \begin{lemma} + \begin{lemma}\label{runninginversion} @{thm runing_inversion} \end{lemma} + explain tRAG + \bigskip + + + Suppose the thread @{term th} is \emph{not} running in state @{term + "t @ s"}, meaning that it should be blocked by some other thread. + It is first shown that there is a path in the RAG leading from node + @{term th} to another thread @{text "th'"}, which is also in the + @{term readys}-set. Since @{term readys}-set is non-empty, there + must be one in it which holds the highest @{term cp}-value, which, + by definition, is currently the @{term running}-thread. However, we + are going to show in the next lemma slightly more: this running + thread is exactly @{term "th'"}. \begin{lemma} - @{thm th_blockedE} + If @{thm (prem 1) th_blockedE_pretty} then + @{thm (concl) th_blockedE_pretty}. \end{lemma} + \begin{proof} + %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the + %thread ``normally'' has). + %So we want to show what the cp of th' is in state t @ s. + %We look at all the assingned precedences in the subgraph starting from th' + %We are looking for the maximum of these assigned precedences. + %This subgraph must contain the thread th, which actually has the highest precednence + %so cp of th' in t @ s has this (assigned) precedence of th + %We know that cp (t @ s) th' + %is the Maximum of the threads in the subgraph starting from th' + %this happens to be the precedence of th + %th has the highest precedence of all threads + \end{proof} + + \begin{corollary} + Using the lemma \ref{runninginversion} we can say more about the thread th' + \end{corollary} + \subsection*{END OUTLINE} diff -r 71a3300d497b -r 95e7933968f8 PIPBasics.thy --- a/PIPBasics.thy Fri Apr 15 14:44:09 2016 +0100 +++ b/PIPBasics.thy Thu Jun 02 13:15:03 2016 +0100 @@ -14,7 +14,7 @@ *} -section {* Generic aulxiliary lemmas *} +section {* Generic auxiliary lemmas *} lemma rel_eqI: assumes "\ x y. (x,y) \ A \ (x,y) \ B" @@ -540,6 +540,11 @@ } ultimately show ?thesis by blast qed +lemma image_eq: + assumes "A = B" + shows "f ` A = f ` B" + using assms by auto + lemma tRAG_trancl_eq_Th: "{Th th' | th'. (Th th', Th th) \ (tRAG s)^+} = {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" @@ -573,7 +578,8 @@ proof assume "Th th' \ Th th \ (Th th', Th th) \ (RAG s)\<^sup>+" with h have "n \ {Th th' | th'. (Th th', Th th) \ (RAG s)^+}" by auto - thus ?thesis using subtree_def tRAG_trancl_eq by fastforce + thus ?thesis using subtree_def tRAG_trancl_eq + by fastforce (* ccc *) qed (insert h, auto simp:subtree_def) } ultimately show ?thesis by auto qed @@ -4874,6 +4880,36 @@ apply(auto) done +lemma detached_cp_the_preced: + assumes "detached s th" + shows "cp s th = the_preced s th" (is "?L = ?R") +proof - + have "?L = Max (the_preced s ` {th'. Th th' \ subtree (RAG s) (Th th)})" + by (unfold cp_alt_def, simp) + moreover have "{th'. Th th' \ subtree (RAG s) (Th th)} = {th}" + proof - + { fix n + assume "n \ subtree (RAG s) (Th th)" + hence "n = Th th" + proof(cases rule:subtreeE) + case 2 + from 2(2) have "Th th \ Range (RAG s)" + by (elim ancestors_Field, simp) + moreover from assms[unfolded detached_test] have "Th th \ Field (RAG s)" . + ultimately have False by (auto simp:Field_def) + thus ?thesis by simp + qed simp + } thus ?thesis by auto + qed + ultimately show ?thesis by auto +qed + +lemma detached_cp_preced: + assumes "detached s th" + shows "cp s th = preced th s" + using detached_cp_the_preced[OF assms] + by (simp add:the_preced_def) + context valid_trace begin @@ -5071,4 +5107,98 @@ end +lemma PIP_actorE: + assumes "PIP s e" + and "actor e = th" + and "\ isCreate e" + shows "th \ runing s" + using assms + by (cases, auto) + + +lemma holdents_RAG: + assumes "holdents s th = {}" + shows "Th th \ Range (RAG s)" +proof + assume "Th th \ Range (RAG s)" + thus False + proof(rule RangeE) + fix a + assume "(a, Th th) \ RAG s" + with assms[unfolded holdents_test] + show False + by (cases a, auto simp:cs_RAG_raw s_RAG_abv) + qed +qed + +lemma readys_RAG: + assumes "th \ readys s" + shows "Th th \ Domain (RAG s)" +proof + assume "Th th \ Domain (RAG s)" + thus False + proof(rule DomainE) + fix b + assume "(Th th, b) \ RAG s" + with assms[unfolded readys_def s_waiting_def] + show False + by (cases b, auto simp:cs_RAG_raw s_RAG_abv cs_waiting_raw) + qed +qed + +lemma readys_holdents_detached: + assumes "th \ readys s" + and "holdents s th = {}" + shows "detached s th" +proof - + from readys_RAG[OF assms(1)] holdents_RAG[OF assms(2)] + show ?thesis + by (unfold detached_test Field_def, auto) +qed + +lemma len_actions_of_sigma: + assumes "finite A" + shows "length (actions_of A t) = (\ th' \ A. length (actions_of {th'} t))" +proof(induct t) + case h: (Cons e t) + thus ?case (is "?L = ?R" is "_ = ?T (e#t)") + proof(cases "actor e \ A") + case True + have "?L = 1 + ?T t" + by (fold h, insert True, simp add:actions_of_def) + moreover have "?R = 1 + ?T t" + proof - + have "?R = length (actions_of {actor e} (e # t)) + + (\th'\A - {actor e}. length (actions_of {th'} (e # t)))" + (is "_ = ?F (e#t) + ?G (e#t)") + by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", + OF assms True], simp) + moreover have "?F (e#t) = 1 + ?F t" using True + by (simp add:actions_of_def) + moreover have "?G (e#t) = ?G t" + by (rule setsum.cong, auto simp:actions_of_def) + moreover have "?F t + ?G t = ?T t" + by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", + OF assms True], simp) + ultimately show ?thesis by simp + qed + ultimately show ?thesis by simp + next + case False + hence "?L = length (actions_of A t)" + by (simp add:actions_of_def) + also have "... = (\th'\A. length (actions_of {th'} t))" by (simp add: h) + also have "... = ?R" + by (rule setsum.cong; insert False, auto simp:actions_of_def) + finally show ?thesis . + qed +qed (auto simp:actions_of_def) + +lemma threads_Exit: + assumes "th \ threads s" + and "th \ threads (e#s)" + shows "e = Exit th" + using assms + by (cases e, auto) + end diff -r 71a3300d497b -r 95e7933968f8 PIPDefs.thy --- a/PIPDefs.thy Fri Apr 15 14:44:09 2016 +0100 +++ b/PIPDefs.thy Thu Jun 02 13:15:03 2016 +0100 @@ -38,12 +38,14 @@ V thread cs | -- {* Thread @{text "thread"} releasing critical resource @{text "cs"}. *} Set thread priority -- {* Thread @{text "thread"} resets its priority to @{text "priority"}. *} -fun actor :: "event \ thread" where - "actor (Create th pty) = th" | +fun actor where "actor (Exit th) = th" | "actor (P th cs) = th" | "actor (V th cs) = th" | - "actor (Set th pty) = th" + "actor (Set th pty) = th" | + "actor (Create th prio) = th" + +definition "actions_of ths s = filter (\ e. actor e \ ths) s" fun isCreate :: "event \ bool" where "isCreate (Create th pty) = True" | diff -r 71a3300d497b -r 95e7933968f8 RTree.thy --- 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) \ r \ a \ subtree r x \ b \ subtree r x}" -proof - - { fix a b - assume h: "(a, b) \ r" "b \ subtree r x" - moreover have "a \ subtree r x" - proof - - from h(2)[unfolded subtree_def] have "(b, x) \ r^*" by simp - with h(1) have "(a, x) \ r^*" by auto - thus ?thesis by (auto simp:subtree_def) - qed - ultimately have "((a, b) \ r \ a \ subtree r x \ b \ 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) \ r" by (auto simp:children_def) - hence "x \ 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 "\ k < j. \ P k" -using assms -proof - - have "\ j. P j \ (\ k < j. \ P k)" using assms - proof(induct i rule:less_induct) - case (less t) - show ?case - proof(cases "\ j < t. \ 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) \ 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) \ 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 \ []" - obtains xs' where "xs = xs'@[y]" -proof - - from append_butlast_last_id[OF `xs \ []`, 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 \ []" 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)} \ edges_on (b # xs)" (is "?L = ?R") -proof - - { fix c d - assume "(c, d) \ ?L" - then obtain l1 l2 where h: "(a # b # xs) = l1 @ [c, d] @ l2" - by (auto simp:edges_on_def) - have "(c, d) \ ?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) \ ?R" - moreover have "(a, b) \ ?L" - proof - - have "(a # b # xs) = []@[a,b]@xs" by simp - hence "\ l1 l2. (a # b # xs) = l1@[a,b]@l2" by auto - thus ?thesis by (unfold edges_on_def, simp) - qed - moreover { - assume "(c, d) \ 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 "\ l1 l2. (a # b # xs) = l1@[c,d]@l2" by metis - hence "(c,d) \ ?L" by (unfold edges_on_def, simp) - } - ultimately have "(c, d) \ ?L" by auto - } ultimately show ?thesis by auto -qed - -lemma edges_on_len: - assumes "(a,b) \ edges_on l" - shows "length l \ 2" +lemma edge_on_headI[simp, intro]: + assumes "(a, b) = (a', b')" + shows "(a, b) \ edges_on (a' # b' # xs)" using assms by (unfold edges_on_def, auto) +lemma edges_on_ConsI[intro]: + assumes "(a, b) \ edges_on xs" + shows "(a, b) \ 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) \ edges_on xs" + shows "(a, b) \ 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) \ edges_on xs" + shows "(a, b) \ edges_on (xs@xs')" + using assms + apply (unfold edges_on_def, auto) + by metis + +lemma edges_onE [elim]: + assumes "(a, b) \ edges_on xs" + obtains a' b' xs' where "(a,b) = (a', b')" "xs = a'#b'#xs'" + | a' b' xs' where "(a,b) \ (a', b')" "xs = a'#b'#xs'" "(a,b) \ 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)} \ edges_on (b # xs)" (is "?L = ?R") +by (auto) + +lemma edges_on_len: + assumes "x \ edges_on l" + shows "2 \ 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) \ edges_on (x#xs)" obtains (head) xs' where "x = a" and "xs = b#xs'" | (tail) "(a,b) \ edges_on xs" -proof - - from assms obtain l1 l2 - where h: "(x#xs) = l1 @ [a,b] @ l2" by (unfold edges_on_def, blast) - have "(\ xs'. x = a \ xs = b#xs') \ ((a,b) \ 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 "(\xs'. x = a \ 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) \ 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)) \ 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) \ edges_on (x # y # ys)" - hence "(a, b) \ r" by (cases, insert rstep, auto) - } thus ?thesis by auto - qed -qed + shows "edges_on (x#xs) \ 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 \ edges_on (x#xs)" -proof - - { fix a b - assume "(a, b) \ 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) \ 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 \ edges_on (xs'@xs)" + by auto + +lemma edges_on_append_mono' [intro,simp]: + shows "edges_on xs \ 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) \ 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) \ r2" - proof - - have "(x, y) \ 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]) \ r" shows "rpath r a (xs@[b]) b" using assms -proof(induct xs arbitrary: a b) - case Nil - moreover have "(a, b) \ edges_on (a # [] @ [b])" - by (unfold edges_on_def, auto) - ultimately have "(a, b) \ r" by auto - thus ?case by auto -next - case (Cons x xs a b) - from this(2) have "edges_on (x # xs @ [b]) \ 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) \ 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 \ []" + obtains x xs' where "xs = xs'@[x]" + by (insert assms, rule rev_exhaust, fastforce) + +lemma edges_on_rpathI' [intro]: + assumes "edges_on (a#xs) \ r" + and "xs \ []" + 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) \ r^*"} *} -lemma star_rpath: + +lemma star_rpath [elim]: assumes "(x, y) \ r^*" obtains xs where "rpath r x xs y" -proof - - have "\ 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) \ r^*"}. *} -lemma rpath_star: +lemma rpath_star [simp]: assumes "rpath r x xs y" shows "(x, y) \ 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 \ r2" + shows "rpath r2 x xs y" + using assms + by (induct, auto) + +lemma subtree_transfer[intro]: assumes "a \ subtree r1 a'" and "r1 \ r2" shows "a \ subtree r2 a'" + using assms proof - - from assms(1)[unfolded subtree_def] - have "(a, a') \ 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) \ 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') \ r1\<^sup>*" . + with assms(2) have "(a, a') \ 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 \ r2" + shows "subtree r1 x \ subtree r2 x" + using assms by auto + +lemma subtree_rev_transfer[intro]: assumes "a \ subtree r2 a'" and "r1 \ r2" shows "a \ 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 \ []" shows "(x, y) \ 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) \ r\<^sup>*" . - with rstep(1) show "(x, y) \ r^+" by auto - qed - qed -qed + using assms + by (induct, simp) fastforce -lemma plus_rpath: +lemma plus_rpath [elim]: assumes "(x, y) \ r^+" obtains xs where "rpath r x xs y" and "xs \ []" 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) \ 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 "\ xs. rpath r x xs y \ xs \ []" 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 \ ancestors r a" shows "a \ subtree r b" using assms by (auto simp:subtree_def ancestors_def) -lemma ancestors_Field: +lemma ancestors_Field[elim]: assumes "b \ ancestors r a" obtains "a \ Domain r" "b \ 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 \ subtree r b" obtains "a = b" | "a \ b" and "b \ ancestors r a" @@ -599,7 +541,7 @@ qed -lemma subtree_Field: +lemma subtree_Field [simp, iff]: "subtree r x \ Field r \ {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 \ b" shows "b \ 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 \ r2" - shows "subtree r1 x \ subtree r2 x" -proof - fix c - assume "c \ subtree r1 x" - hence "(c, x) \ 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) \ r1" . - with assms show "edges_on (c # xs) \ r2" by auto - qed - thus "c \ 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 \ 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 \ 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 \ (subtree r x)" + assume "c \ ?R" hence "(c, x) \ r^*" by (auto simp:subtree_def) - hence "c \ subtree (r - {(a, b)}) x" + hence "c \ ?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) \ r" . + from rp have "edges_on (c # xs) \ r" .. moreover have "(a, b) \ edges_on (c#xs)" proof assume "(a, b) \ 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) \ r - {(a,b)}" by auto + ultimately show "edges_on (c # xs) \ (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 \ subtree (r - {(a, b)}) x" - moreover have "... \ (subtree r x)" by (rule subtree_mono, auto) - ultimately have "c \ (subtree r x)" by auto + assume "c \ ?L" + moreover have "... \ (subtree r x)" by auto + ultimately have "c \ ?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' \ 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) \ r" . + from rp have "edges_on (c # xs) \ r" .. moreover { fix a b assume h: "(a, b) \ r'" @@ -731,7 +649,7 @@ with assms (1) and h show ?thesis by (auto) qed qed - } ultimately show "edges_on (c # xs) \ r - r'" by auto + } ultimately show "edges_on (c # xs) \ (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 \ subtree r x" shows "subtree (r \ {(a, b)}) x = (subtree r x) \ (subtree r a)" using assms by (auto simp:subtree_def rtrancl_insert) -lemma subtree_insert_next: +lemma subtree_insert_next [simp, intro]: assumes "b \ subtree r x" shows "subtree (r \ {(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 \ Domain r1" shows "root (r \ r1) a" + using assms proof - let ?r = "r \ r1" { fix a' @@ -777,7 +696,7 @@ } thus ?thesis by (auto simp:root_def) qed -lemma ancestors_mono: +lemma ancestors_mono [simp]: assumes "r1 \ r2" shows "ancestors r1 x \ ancestors r2 x" proof @@ -788,8 +707,9 @@ h: "rpath r1 x xs a" "xs \ []" . 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) \ r2" by auto + from h(1) have "edges_on (x # xs) \ r1" .. + also note assms + finally show "edges_on (x # xs) \ r2" . qed from rpath_plus[OF this h(2)] show "a \ 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: "\ x'. x' \ x \ x \ subtree r' x'" and "r' \ 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 \ 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) \ r" proof - from eq_xs1[unfolded eq_es] have "xs1 = es@[e, xs1!?idx]@drop (Suc ?idx) xs1" by simp hence "(e, xs1!?idx) \ 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) \ 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) \ 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) \ 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 \ 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) \ 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 \ ancestors r z \ z \ \(subtree r ` children r x)" + by (unfold ancestors_def children_def, auto simp:subtree_def dest:tranclD2) + +lemma [iff]: "x \ subtree r x" + by (auto simp:subtree_def) + +lemma [intro]: "xa \ children r x \ z \ subtree r xa \ z \ subtree r x" + by (unfold children_def subtree_def, auto) lemma subtree_children: - "subtree r x = {x} \ (\ (subtree r ` (children r x)))" (is "?L = ?R") -proof - - { fix z - assume "z \ ?L" - hence "z \ ?R" - proof(cases rule:subtreeE[consumes 1]) - case 2 - hence "(z, x) \ r^+" by (auto simp:ancestors_def) - thus ?thesis - proof(rule tranclE) - assume "(z, x) \ r" - hence "z \ children r x" by (unfold children_def, auto) - moreover have "z \ subtree r z" by (auto simp:subtree_def) - ultimately show ?thesis by auto - next - fix c - assume h: "(z, c) \ r\<^sup>+" "(c, x) \ r" - hence "c \ children r x" by (auto simp:children_def) - moreover from h have "z \ subtree r c" by (auto simp:subtree_def) - ultimately show ?thesis by auto - qed - qed auto - } moreover { - fix z - assume h: "z \ ?R" - have "x \ subtree r x" by (auto simp:subtree_def) - moreover { - assume "z \ \(subtree r ` children r x)" - then obtain y where "(y, x) \ r" "(z, y) \ r^*" - by (auto simp:subtree_def children_def) - hence "(z, x) \ r^*" by auto - hence "z \ ?L" by (auto simp:subtree_def) - } ultimately have "z \ ?L" using h by auto - } ultimately show ?thesis by auto -qed + "subtree r x = ({x} \ (\ (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 \ r" and "r2 \ r" shows "r1 O r2 \ 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 \ r" and "r2 \ r" @@ -1724,7 +1616,7 @@ "children (r1 O r2) x = \ (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 \ 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 \ subtree r x" by (auto simp:children_def subtree_def) -lemma children_union_kept: +lemma children_union_kept [simp]: assumes "x \ Range r'" shows "children (r \ 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) \ r^*" "\ c. (c, b) \ 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 \ Range r" obtains b where "(b, a) \ r^+" "\ c. (c, b) \ 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 diff -r 71a3300d497b -r 95e7933968f8 journal.pdf Binary file journal.pdf has changed