pip: comparison PrioG.thy

equal deleted inserted replaced

-:8f026b608378
+:e861aff29655
 using assms
 unfolding s_holding_def
 by auto
-lemma birthtime_lt: "th \<in> threads s \<Longrightarrow> birthtime th s < length s"
+lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"
 apply (induct s, auto)
 by (case_tac a, auto split:if_splits)
-lemma birthtime_unique:
+lemma last_set_unique:
-"\<lbrakk>birthtime th1 s = birthtime th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
+"\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
 \<Longrightarrow> th1 = th2"
 apply (induct s, auto)
-by (case_tac a, auto split:if_splits dest:birthtime_lt)
+by (case_tac a, auto split:if_splits dest:last_set_lt)
 lemma preced_unique :
 assumes pcd_eq: "preced th1 s = preced th2 s"
 and th_in1: "th1 \<in> threads s"
 and th_in2: " th2 \<in> threads s"
 shows "th1 = th2"
 proof -
-from pcd_eq have "birthtime th1 s = birthtime th2 s" by (simp add:preced_def)
+from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)
-from birthtime_unique [OF this th_in1 th_in2]
+from last_set_unique [OF this th_in1 th_in2]
 show ?thesis .
 qed
 lemma preced_linorder:
 assumes neq_12: "th1 \<noteq> th2"
 and runing_2: "th2 \<in> runing s"
 shows "th1 = th2"
 proof -
 from runing_1 and runing_2 have "cp s th1 = cp s th2"
 by (unfold runing_def, simp)
-hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1)) =
+hence eq_max: "Max ((\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)) =
-Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependents (wq s) th2))"
+Max ((\<lambda>th. preced th s) ` ({th2} \<union> dependants (wq s) th2))"
 (is "Max (?f ` ?A) = Max (?f ` ?B)")
 by (unfold cp_eq_cpreced cpreced_def)
 obtain th1' where th1_in: "th1' \<in> ?A" and eq_f_th1: "?f th1' = Max (?f ` ?A)"
 proof -
 have h1: "finite (?f ` ?A)"
 proof -
 have "finite ?A"
 proof -
-have "finite (dependents (wq s) th1)"
+have "finite (dependants (wq s) th1)"
 proof-
 have "finite {th'. (Th th', Th th1) \<in> (depend (wq s))\<^sup>+}"
 proof -
 let ?F = "\<lambda> (x, y). the_th x"
 have "{th'. (Th th', Th th1) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (wq s))\<^sup>+)"
 by (auto simp: s_depend_def cs_depend_def wq_def)
 thus ?thesis by auto
 qed
 ultimately show ?thesis by (auto intro:finite_subset)
 qed
-thus ?thesis by (simp add:cs_dependents_def)
+thus ?thesis by (simp add:cs_dependants_def)
 qed
 thus ?thesis by simp
 qed
 thus ?thesis by auto
 qed
 proof -
 have h1: "finite (?f ` ?B)"
 proof -
 have "finite ?B"
 proof -
-have "finite (dependents (wq s) th2)"
+have "finite (dependants (wq s) th2)"
 proof-
 have "finite {th'. (Th th', Th th2) \<in> (depend (wq s))\<^sup>+}"
 proof -
 let ?F = "\<lambda> (x, y). the_th x"
 have "{th'. (Th th', Th th2) \<in> (depend (wq s))\<^sup>+} \<subseteq> ?F ` ((depend (wq s))\<^sup>+)"
 by (auto simp: s_depend_def cs_depend_def wq_def)
 thus ?thesis by auto
 qed
 ultimately show ?thesis by (auto intro:finite_subset)
 qed
-thus ?thesis by (simp add:cs_dependents_def)
+thus ?thesis by (simp add:cs_dependants_def)
 qed
 thus ?thesis by simp
 qed
 thus ?thesis by auto
 qed
 qed
 from eq_f_th1 eq_f_th2 eq_max
 have eq_preced: "preced th1' s = preced th2' s" by auto
 hence eq_th12: "th1' = th2'"
 proof (rule preced_unique)
-from th1_in have "th1' = th1 \<or> (th1' \<in> dependents (wq s) th1)" by simp
+from th1_in have "th1' = th1 \<or> (th1' \<in> dependants (wq s) th1)" by simp
 thus "th1' \<in> threads s"
 proof
-assume "th1' \<in> dependents (wq s) th1"
+assume "th1' \<in> dependants (wq s) th1"
 hence "(Th th1') \<in> Domain ((depend s)^+)"
-apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+apply (unfold cs_dependants_def cs_depend_def s_depend_def)
 by (auto simp:Domain_def)
 hence "(Th th1') \<in> Domain (depend s)" by (simp add:trancl_domain)
 from dm_depend_threads[OF vt this] show ?thesis .
 next
 assume "th1' = th1"
 with runing_1 show ?thesis
 by (unfold runing_def readys_def, auto)
 qed
 next
-from th2_in have "th2' = th2 \<or> (th2' \<in> dependents (wq s) th2)" by simp
+from th2_in have "th2' = th2 \<or> (th2' \<in> dependants (wq s) th2)" by simp
 thus "th2' \<in> threads s"
 proof
-assume "th2' \<in> dependents (wq s) th2"
+assume "th2' \<in> dependants (wq s) th2"
 hence "(Th th2') \<in> Domain ((depend s)^+)"
-apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+apply (unfold cs_dependants_def cs_depend_def s_depend_def)
 by (auto simp:Domain_def)
 hence "(Th th2') \<in> Domain (depend s)" by (simp add:trancl_domain)
 from dm_depend_threads[OF vt this] show ?thesis .
 next
 assume "th2' = th2"
 with runing_2 show ?thesis
 by (unfold runing_def readys_def, auto)
 qed
 qed
-from th1_in have "th1' = th1 \<or> th1' \<in> dependents (wq s) th1" by simp
+from th1_in have "th1' = th1 \<or> th1' \<in> dependants (wq s) th1" by simp
 thus ?thesis
 proof
 assume eq_th': "th1' = th1"
-from th2_in have "th2' = th2 \<or> th2' \<in> dependents (wq s) th2" by simp
+from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp
 thus ?thesis
 proof
 assume "th2' = th2" thus ?thesis using eq_th' eq_th12 by simp
 next
-assume "th2' \<in> dependents (wq s) th2"
+assume "th2' \<in> dependants (wq s) th2"
-with eq_th12 eq_th' have "th1 \<in> dependents (wq s) th2" by simp
+with eq_th12 eq_th' have "th1 \<in> dependants (wq s) th2" by simp
 hence "(Th th1, Th th2) \<in> (depend s)^+"
-by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
 hence "Th th1 \<in> Domain ((depend s)^+)"
-apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+apply (unfold cs_dependants_def cs_depend_def s_depend_def)
 by (auto simp:Domain_def)
 hence "Th th1 \<in> Domain (depend s)" by (simp add:trancl_domain)
 then obtain n where d: "(Th th1, n) \<in> depend s" by (auto simp:Domain_def)
 from depend_target_th [OF this]
 obtain cs' where "n = Cs cs'" by auto
 apply (unfold runing_def readys_def s_depend_def)
 by (auto simp:eq_waiting)
 thus ?thesis by simp
 qed
 next
-assume th1'_in: "th1' \<in> dependents (wq s) th1"
+assume th1'_in: "th1' \<in> dependants (wq s) th1"
-from th2_in have "th2' = th2 \<or> th2' \<in> dependents (wq s) th2" by simp
+from th2_in have "th2' = th2 \<or> th2' \<in> dependants (wq s) th2" by simp
 thus ?thesis
 proof
 assume "th2' = th2"
-with th1'_in eq_th12 have "th2 \<in> dependents (wq s) th1" by simp
+with th1'_in eq_th12 have "th2 \<in> dependants (wq s) th1" by simp
 hence "(Th th2, Th th1) \<in> (depend s)^+"
-by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
 hence "Th th2 \<in> Domain ((depend s)^+)"
-apply (unfold cs_dependents_def cs_depend_def s_depend_def)
+apply (unfold cs_dependants_def cs_depend_def s_depend_def)
 by (auto simp:Domain_def)
 hence "Th th2 \<in> Domain (depend s)" by (simp add:trancl_domain)
 then obtain n where d: "(Th th2, n) \<in> depend s" by (auto simp:Domain_def)
 from depend_target_th [OF this]
 obtain cs' where "n = Cs cs'" by auto
 with runing_2 have "False"
 apply (unfold runing_def readys_def s_depend_def)
 by (auto simp:eq_waiting)
 thus ?thesis by simp
 next
-assume "th2' \<in> dependents (wq s) th2"
+assume "th2' \<in> dependants (wq s) th2"
-with eq_th12 have "th1' \<in> dependents (wq s) th2" by simp
+with eq_th12 have "th1' \<in> dependants (wq s) th2" by simp
 hence h1: "(Th th1', Th th2) \<in> (depend s)^+"
-by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
 from th1'_in have h2: "(Th th1', Th th1) \<in> (depend s)^+"
-by (unfold cs_dependents_def s_depend_def cs_depend_def, simp)
+by (unfold cs_dependants_def s_depend_def cs_depend_def, simp)
 show ?thesis
 proof(rule dchain_unique[OF vt h1 _ h2, symmetric])
 from runing_1 show "th1 \<in> readys s" by (simp add:runing_def)
 from runing_2 show "th2 \<in> readys s" by (simp add:runing_def)
 qed
 lemma eq_depend:
 "depend (wq s) = depend s"
 by (unfold cs_depend_def s_depend_def, auto)
-lemma count_eq_dependents:
+lemma count_eq_dependants:
 assumes vt: "vt s"
 and eq_pv: "cntP s th = cntV s th"
-shows "dependents (wq s) th = {}"
+shows "dependants (wq s) th = {}"
 proof -
 from cnp_cnv_cncs[OF vt] and eq_pv
 have "cntCS s th = 0"
 by (auto split:if_splits)
 moreover have "finite {cs. (Cs cs, Th th) \<in> depend s}"
 proof -
 from finite_holding[OF vt, of th] show ?thesis
 by (simp add:holdents_test)
 qed
 ultimately have h: "{cs. (Cs cs, Th th) \<in> depend s} = {}"
-by (unfold cntCS_def holdents_test cs_dependents_def, auto)
+by (unfold cntCS_def holdents_test cs_dependants_def, auto)
 show ?thesis
-proof(unfold cs_dependents_def)
+proof(unfold cs_dependants_def)
 { assume "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}"
 then obtain th' where "(Th th', Th th) \<in> (depend (wq s))\<^sup>+" by auto
 hence "False"
 proof(cases)
 assume "(Th th', Th th) \<in> depend (wq s)"
 qed
 } thus "{th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} = {}" by auto
 qed
 qed
-lemma dependents_threads:
+lemma dependants_threads:
 fixes s th
 assumes vt: "vt s"
-shows "dependents (wq s) th \<subseteq> threads s"
+shows "dependants (wq s) th \<subseteq> threads s"
 proof
 { fix th th'
 assume h: "th \<in> {th'a. (Th th'a, Th th') \<in> (depend (wq s))\<^sup>+}"
 have "Th th \<in> Domain (depend s)"
 proof -
 qed
 from dm_depend_threads[OF vt this]
 have "th \<in> threads s" .
 } note hh = this
 fix th1
-assume "th1 \<in> dependents (wq s) th"
+assume "th1 \<in> dependants (wq s) th"
 hence "th1 \<in> {th'a. (Th th'a, Th th) \<in> (depend (wq s))\<^sup>+}"
-by (unfold cs_dependents_def, simp)
+by (unfold cs_dependants_def, simp)
 from hh [OF this] show "th1 \<in> threads s" .
 qed
 lemma finite_threads:
 assumes vt: "vt s"
 lemma cp_le:
 assumes vt: "vt s"
 and th_in: "th \<in> threads s"
 shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
-proof(unfold cp_eq_cpreced cpreced_def cs_dependents_def)
+proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
 show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+}))
 \<le> Max ((\<lambda>th. preced th s) ` threads s)"
 (is "Max (?f ` ?A) \<le> Max (?f ` ?B)")
 proof(rule Max_f_mono)
 show "{th} \<union> {th'. (Th th', Th th) \<in> (depend (wq s))\<^sup>+} \<noteq> {}" by simp
 lemma le_cp:
 assumes vt: "vt s"
 shows "preced th s \<le> cp s th"
 proof(unfold cp_eq_cpreced preced_def cpreced_def, simp)
-show "Prc (original_priority th s) (birthtime th s)
+show "Prc (priority th s) (last_set th s)
-\<le> Max (insert (Prc (original_priority th s) (birthtime th s))
+\<le> Max (insert (Prc (priority th s) (last_set th s))
-((\<lambda>th. Prc (original_priority th s) (birthtime th s)) ` dependents (wq s) th))"
+((\<lambda>th. Prc (priority th s) (last_set th s)) ` dependants (wq s) th))"
 (is "?l \<le> Max (insert ?l ?A)")
 proof(cases "?A = {}")
 case False
 have "finite ?A" (is "finite (?f ` ?B)")
 proof -
 by (auto simp: s_depend_def cs_depend_def wq_def)
 thus ?thesis by auto
 qed
 ultimately show ?thesis by (auto intro:finite_subset)
 qed
-thus ?thesis by (simp add:cs_dependents_def)
+thus ?thesis by (simp add:cs_dependants_def)
 qed
 thus ?thesis by simp
 qed
 from Max_insert [OF this False, of ?l] show ?thesis by auto
 next
 assume "\<exists>th'. th' \<in> readys s \<and> (Th tm, Th th') \<in> (depend s)\<^sup>+ "
 then obtain th' where th'_in: "th' \<in> readys s"
 and tm_chain:"(Th tm, Th th') \<in> (depend s)\<^sup>+" by auto
 have "cp s th' = ?f tm"
 proof(subst cp_eq_cpreced, subst cpreced_def, rule Max_eqI)
-from dependents_threads[OF vt] finite_threads[OF vt]
+from dependants_threads[OF vt] finite_threads[OF vt]
-show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th'))"
+show "finite ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th'))"
 by (auto intro:finite_subset)
 next
-fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')"
+fix p assume p_in: "p \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"
 from tm_max have " preced tm s = Max ((\<lambda>th. preced th s) ` threads s)" .
 moreover have "p \<le> \<dots>"
 proof(rule Max_ge)
 from finite_threads[OF vt]
 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
 next
-from p_in and th'_in and dependents_threads[OF vt, of th']
+from p_in and th'_in and dependants_threads[OF vt, of th']
 show "p \<in> (\<lambda>th. preced th s) ` threads s"
 by (auto simp:readys_def)
 qed
 ultimately show "p \<le> preced tm s" by auto
 next
-show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')"
+show "preced tm s \<in> (\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')"
 proof -
 from tm_chain
-have "tm \<in> dependents (wq s) th'"
+have "tm \<in> dependants (wq s) th'"
-by (unfold cs_dependents_def s_depend_def cs_depend_def, auto)
+by (unfold cs_dependants_def s_depend_def cs_depend_def, auto)
 thus ?thesis by auto
 qed
 qed
 with tm_max
 have h: "cp s th' = Max ((\<lambda>th. preced th s) ` threads s)" by simp
 show "q \<le> cp s th'"
 apply (unfold h eq_q)
 apply (unfold cp_eq_cpreced cpreced_def)
 apply (rule Max_mono)
 proof -
-from dependents_threads [OF vt, of th1] th1_in
+from dependants_threads [OF vt, of th1] th1_in
-show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1) \<subseteq>
+show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<subseteq>
 (\<lambda>th. preced th s) ` threads s"
 by (auto simp:readys_def)
 next
-show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1) \<noteq> {}" by simp
+show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}" by simp
 next
 from finite_threads[OF vt]
 show " finite ((\<lambda>th. preced th s) ` threads s)" by simp
 qed
 next
 show ?thesis
 proof(fold tm_max)
 have cp_eq_p: "cp s tm = preced tm s"
 proof(unfold cp_eq_cpreced cpreced_def, rule Max_eqI)
 fix y
-assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm)"
+assume hy: "y \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"
 show "y \<le> preced tm s"
 proof -
 { fix y'
-assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependents (wq s) tm)"
+assume hy' : "y' \<in> ((\<lambda>th. preced th s) ` dependants (wq s) tm)"
 have "y' \<le> preced tm s"
 proof(unfold tm_max, rule Max_ge)
-from hy' dependents_threads[OF vt, of tm]
+from hy' dependants_threads[OF vt, of tm]
 show "y' \<in> (\<lambda>th. preced th s) ` threads s" by auto
 next
 from finite_threads[OF vt]
 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
 qed
 } with hy show ?thesis by auto
 qed
 next
-from dependents_threads[OF vt, of tm] finite_threads[OF vt]
+from dependants_threads[OF vt, of tm] finite_threads[OF vt]
-show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm))"
+show "finite ((\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm))"
 by (auto intro:finite_subset)
 next
-show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependents (wq s) tm)"
+show "preced tm s \<in> (\<lambda>th. preced th s) ` ({tm} \<union> dependants (wq s) tm)"
 by simp
 qed
 moreover have "Max (cp s ` readys s) = cp s tm"
 proof(rule Max_eqI)
 from tm_ready show "cp s tm \<in> cp s ` readys s" by simp
 apply(unfold cp_eq_cpreced cpreced_def tm_max, rule Max_mono)
 proof -
 from finite_threads[OF vt]
 show "finite ((\<lambda>th. preced th s) ` threads s)" by simp
 next
-show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1) \<noteq> {}"
+show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1) \<noteq> {}"
 by simp
 next
-from dependents_threads[OF vt, of th1] th1_readys
+from dependants_threads[OF vt, of th1] th1_readys
-show "(\<lambda>th. preced th s) ` ({th1} \<union> dependents (wq s) th1)
+show "(\<lambda>th. preced th s) ` ({th1} \<union> dependants (wq s) th1)
 \<subseteq> (\<lambda>th. preced th s) ` threads s"
 by (auto simp:readys_def)
 qed
 qed
 ultimately show " Max (cp s ` readys s) = preced tm s" by simp

changeset 32	e861aff29655
parent 3	51019d035a79
child 35	92f61f6a0fe7