364   shows "isP e \<and> actor e = th"

   364   obtains cs where "e = P th cs"

   367   show ?thesis

   367   show ?thesis using that

   374   shows "isV e \<and> actor e = th"

   374   obtains cs' where "e = V th cs'"

   377   show ?thesis

   377   show ?thesis using that

  4922 section {* Other properties useful in Implementation.thy or Correctness.thy *}

  4927 section {* Recursive calculation of @{term "cp"} *}

  4923 

  4928 

  4924 context valid_trace_e 

  4929 text {*

  4925 begin

  4930   According to the normal definitions, such as @{thm cp_def}, @{thm cp_alt_def}

  4926 

  4931   and @{thm cp_alt_def1}, the @{term cp}-value of a thread depends 

  4927 lemma actor_inv: 

  4932   on the @{term preced}-values of all threads in its subtree. To calculate 

  4928   assumes "\<not> isCreate e"

  4933   a @{term cp}-value, one needs to traverse a whole subtree. 

  4929   shows "actor e \<in> runing s"

  4934 

  4930   using pip_e assms 

  4935   However, in this section, we are going to show that @{term cp}-value 

  4931   by (induct, auto)

  4936   can be calculate locally (given by the lemma @{text "cp_rec"} in the following).

  4932 end

  4937   According to this lemma,  the @{term cp}-value of a thread can be calculated only from 

  4938   the @{term cp}-values of its children in @{term RAG}. 

  4939   Therefore, if the @{term cp}-values of one thread's children are not

  4940   changed by an execution step, there is no need to recalculate. This

  4941   is particularly useful to in Implementation.thy to speed up the 

  4942   recalculation of @{term cp}-values. 

  4943 *}

  4944 

  4945 text {*

  4946   The following function @{text "cp_gen"} is a generalization 

  4947   of @{term cp}. Unlike @{term cp} which returns a precedence 

  4948   for a thread, @{text "cp_gen"} returns precedence for a node

  4949   in @{term RAG}. When the node represent a thread, @{text cp_gen} is

  4950   coincident with @{term cp} (to be shown in lemma @{text "cp_gen_def_cond"}), 

  4951   and this is the only meaningful use of @{text cp_gen}. 

  4952 

  4953   The introduction of @{text cp_gen} is purely technical to easy some

  4954   of the proofs leading to the finally lemma @{text cp_rec}.

  4955 *}

  4956 

  4957 definition "cp_gen s x =

  4958                   Max ((the_preced s \<circ> the_thread) ` subtree (tRAG s) x)"

  4959 

  4960 lemma cp_gen_alt_def:

  4961   "cp_gen s = (Max \<circ> (\<lambda>x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x))"

  4962     by (auto simp:cp_gen_def)

  4963 

  4964 lemma cp_gen_def_cond: 

  4965   assumes "x = Th th"

  4966   shows "cp s th = cp_gen s (Th th)"

  4967 by (unfold cp_alt_def1 cp_gen_def, simp)

  4968 

  4969 lemma cp_gen_over_set:

  4970   assumes "\<forall> x \<in> A. \<exists> th. x = Th th"

  4971   shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"

  4972 proof(rule f_image_eq)

  4973   fix a

  4974   assume "a \<in> A"

  4975   from assms[rule_format, OF this]

  4976   obtain th where eq_a: "a = Th th" by auto

  4977   show "cp_gen s a = (cp s \<circ> the_thread) a"

  4978     by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)

  4979 qed

  4980 

  4936 

  4984 (* ddd *)

  4937 lemma readys_root:

  4985 lemma cp_gen_rec:

  4938   assumes "th \<in> readys s"

  4986   assumes "x = Th th"

  4939   shows "root (RAG s) (Th th)"

  4987   shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"

  4940 proof -

  4988 proof(cases "children (tRAG s) x = {}")

  4941   { fix x

  4989   case True

  4942     assume "x \<in> ancestors (RAG s) (Th th)"

  4990   show ?thesis

  4943     hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)

  4991     by (unfold True cp_gen_def subtree_children, simp add:assms)

  4944     from tranclD[OF this]

  4992 next

  4945     obtain z where "(Th th, z) \<in> RAG s" by auto

  4993   case False

  4946     with assms(1) have False

  4994   hence [simp]: "children (tRAG s) x \<noteq> {}" by auto

  4947          apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)

  4995   note fsbttRAGs.finite_subtree[simp]

  4948          by (fold wq_def, blast)

  4996   have [simp]: "finite (children (tRAG s) x)"

  4949   } thus ?thesis by (unfold root_def, auto)

  4997      by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], 

  4950 qed

  4998             rule children_subtree)

  4951 

  4999   { fix r x

  4952 lemma readys_in_no_subtree:

  5000     have "subtree r x \<noteq> {}" by (auto simp:subtree_def)

  4953   assumes "th \<in> readys s"

  5001   } note this[simp]

  4954   and "th' \<noteq> th"

  5002   have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}"

  4955   shows "Th th \<notin> subtree (RAG s) (Th th')" 

  5003   proof -

  4956 proof

  5004     from False obtain q where "q \<in> children (tRAG s) x" by blast

  4957    assume "Th th \<in> subtree (RAG s) (Th th')"

  5005     moreover have "subtree (tRAG s) q \<noteq> {}" by simp

  4958    thus False

  5006     ultimately show ?thesis by blast

  4959    proof(cases rule:subtreeE)

  5007   qed

  4960       case 1

  5008   have h: "Max ((the_preced s \<circ> the_thread) `

  4961       with assms show ?thesis by auto

  5009                 ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) =

  4962    next

  5010         Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)"

  4963       case 2

  5011                      (is "?L = ?R")

  4964       with readys_root[OF assms(1)]

  5012   proof -

  4965       show ?thesis by (auto simp:root_def)

  5013     let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L

  4966    qed

  5014     let "Max (_ \<union> (?h ` ?B))" = ?R

  4967 qed

  5015     let ?L1 = "?f ` \<Union>(?g ` ?B)"

  4968 

  5016     have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)"

  4969 lemma not_in_thread_isolated:

  5017     proof -

  4970   assumes "th \<notin> threads s"

  5018       have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp

  4971   shows "(Th th) \<notin> Field (RAG s)"

  5019       also have "... =  (\<Union> x \<in> ?B. ?f ` (?g x))" by auto

  4972 proof

  5020       finally have "Max ?L1 = Max ..." by simp

  4973   assume "(Th th) \<in> Field (RAG s)"

  5021       also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"

  4974   with dm_RAG_threads and rg_RAG_threads assms

  5022         by (subst Max_UNION, simp+)

  4975   show False by (unfold Field_def, blast)

  5023       also have "... = Max (cp_gen s ` children (tRAG s) x)"

  4976 qed

  5024           by (unfold image_comp cp_gen_alt_def, simp)

  4977 

  5025       finally show ?thesis .

  4978 lemma next_th_holding:

  5026     qed

  4979   assumes nxt: "next_th s th cs th'"

  5027     show ?thesis

  4980   shows "holding (wq s) th cs"

  5028     proof -

  4981 proof -

  5029       have "?L = Max (?f ` ?A \<union> ?L1)" by simp

  4982   from nxt[unfolded next_th_def]

  5030       also have "... = max (the_preced s (the_thread x)) (Max ?L1)"

  4983   obtain rest where h: "wq s cs = th # rest"

  5031             by (subst Max_Un, simp+)

  4984                        "rest \<noteq> []" 

  5032       also have "... = max (?f x) (Max (?h ` ?B))"

  4985                        "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto

  5033         by (unfold eq_Max_L1, simp)

  4986   thus ?thesis

  5034       also have "... =?R"

  4987     by (unfold cs_holding_def, auto)

  5035         by (rule max_Max_eq, (simp)+, unfold assms, simp)

  4988 qed

  5036       finally show ?thesis .

  4989 

  5037     qed

  4990 lemma next_th_waiting:

  5038   qed  thus ?thesis 

  4991   assumes nxt: "next_th s th cs th'"

  5039           by (fold h subtree_children, unfold cp_gen_def, simp) 

  4992   shows "waiting (wq s) th' cs"

  5040 qed

  4993 proof -

  5041 

  4994   from nxt[unfolded next_th_def]

  5042 lemma cp_rec:

  4995   obtain rest where h: "wq s cs = th # rest"

  5043   "cp s th = Max ({the_preced s th} \<union> 

  4996                        "rest \<noteq> []" 

  5044                      (cp s o the_thread) ` children (tRAG s) (Th th))"

  4997                        "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto

  5045 proof -

  4998   from wq_distinct[of cs, unfolded h]

  5046   have "Th th = Th th" by simp

  4999   have dst: "distinct (th # rest)" .

  5047   note h =  cp_gen_def_cond[OF this] cp_gen_rec[OF this]

  5000   have in_rest: "th' \<in> set rest"

  5048   show ?thesis 

  5001   proof(unfold h, rule someI2)

  5049   proof -

  5002     show "distinct rest \<and> set rest = set rest" using dst by auto

  5050     have "cp_gen s ` children (tRAG s) (Th th) = 

  5003   next

  5051                 (cp s \<circ> the_thread) ` children (tRAG s) (Th th)"

  5004     fix x assume "distinct x \<and> set x = set rest"

  5052     proof(rule cp_gen_over_set)

  5005     with h(2)

  5053       show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th"

  5006     show "hd x \<in> set (rest)" by (cases x, auto)

  5054         by (unfold tRAG_alt_def, auto simp:children_def)

  5007   qed

  5055     qed

  5008   hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)

  5056     thus ?thesis by (subst (1) h(1), unfold h(2), simp)

  5009   moreover have "th' \<noteq> hd (wq s cs)"

  5057   qed

  5010     by (unfold h(1), insert in_rest dst, auto)

  5058 qed

  5011   ultimately show ?thesis by (auto simp:cs_waiting_def)

  5059 

  5012 qed

  5060 end

  5013 

  5061 

  5014 lemma next_th_RAG:

  5062 end

  5015   assumes nxt: "next_th (s::event list) th cs th'"

  5016   shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"

  5017   using vt assms next_th_holding next_th_waiting

  5018   by (unfold s_RAG_def, simp)

  5019 

  5020 end

  5021 

  5022 end