regexp: comparison prio/CpsG.thy

equal deleted inserted replaced

-:0a4be67ea7f8
+:f2e0d031a395
 imports PrioG
 begin
 lemma not_thread_holdents:
 fixes th s
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and not_in: "th \<notin> threads s"
 shows "holdents s th = {}"
 proof -
 from vt not_in show ?thesis
 proof(induct arbitrary:th)
 case (vt_cons s e th)
-assume vt: "vt step s"
+assume vt: "vt s"
 and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"
 and stp: "step s e"
 and not_in: "th \<notin> threads (e # s)"
 from stp show ?case
 proof(cases)
 qed
 next
 case (thread_P thread cs)
 assume eq_e: "e = P thread cs"
 and is_runing: "thread \<in> runing s"
-from prems have vtp: "vt step (P thread cs#s)" by auto
+from prems have vtp: "vt (P thread cs#s)" by auto
 have neq_th: "th \<noteq> thread"
 proof -
 from not_in eq_e have "th \<notin> threads s" by simp
 moreover from is_runing have "thread \<in> threads s"
 by (simp add:runing_def readys_def)
 from not_in eq_e have "th \<notin> threads s" by simp
 moreover from is_runing have "thread \<in> threads s"
 by (simp add:runing_def readys_def)
 ultimately show ?thesis by auto
 qed
-from prems have vtv: "vt step (V thread cs#s)" by auto
+from prems have vtv: "vt (V thread cs#s)" by auto
 from hold obtain rest
 where eq_wq: "wq s cs = thread # rest"
-by (case_tac "wq s cs", auto simp:s_holding_def)
+by (case_tac "wq s cs", auto simp: wq_def s_holding_def)
 from not_in eq_e eq_wq
 have "\<not> next_th s thread cs th"
 apply (auto simp:next_th_def)
 proof -
 assume ne: "rest \<noteq> []"
 qed
 lemma next_th_neq:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and nt: "next_th s th cs th'"
 shows "th' \<noteq> th"
 proof -
 from nt show ?thesis
 apply (auto simp:next_th_def)
 lemma pp_sub: "(r^+)^+ \<subseteq> r^+"
 by auto
 lemma wf_depend:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "wf (depend s)"
 proof(rule finite_acyclic_wf)
 from finite_depend[OF vt] show "finite (depend s)" .
 next
 from acyclic_depend[OF vt] show "acyclic (depend s)" .
 lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"
 by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)
 lemma child_unique:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and ch1: "(Th th, Th th1) \<in> child s"
 and ch2: "(Th th, Th th2) \<in> child s"
 shows "th1 = th2"
 proof -
 from ch1 ch2 show ?thesis
 lemma sub_child: "child s \<subseteq> (depend s)^+"
 by (unfold child_def, auto)
 lemma wf_child:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "wf (child s)"
 proof(rule wf_subset)
 from wf_trancl[OF wf_depend[OF vt]]
 show "wf ((depend s)\<^sup>+)" .
 next
 from sub_child show "child s \<subseteq> (depend s)\<^sup>+" .
 qed
 lemma depend_child_pre:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows
 "(Th th, n) \<in> (depend s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")
 proof -
 from wf_trancl[OF wf_depend[OF vt]]
 have wf: "wf ((depend s)^+)" .
 qed
 qed
 qed
 qed
-lemma depend_child: "\<lbrakk>vt step s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
+lemma depend_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (depend s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"
 by (insert depend_child_pre, auto)
 lemma child_depend_p:
 assumes "(n1, n2) \<in> (child s)^+"
 shows "(n1, n2) \<in> (depend s)^+"
 ultimately show ?case by auto
 qed
 qed
 lemma child_depend_eq:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows
 "((Th th1, Th th2) \<in> (child s)^+) =
 ((Th th1, Th th2) \<in> (depend s)^+)"
 by (auto intro: depend_child[OF vt] child_depend_p)
 lemma children_no_dep:
 fixes s th th1 th2 th3
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and ch1: "(Th th1, Th th) \<in> child s"
 and ch2: "(Th th2, Th th) \<in> child s"
 and ch3: "(Th th1, Th th2) \<in> (depend s)^+"
 shows "False"
 proof -
 ultimately show False by auto
 qed
 qed
 lemma unique_depend_p:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and dp1: "(n, n1) \<in> (depend s)^+"
 and dp2: "(n, n2) \<in> (depend s)^+"
 and neq: "n1 \<noteq> n2"
 shows "(n1, n2) \<in> (depend s)^+ \<or> (n2, n1) \<in> (depend s)^+"
 proof(rule unique_chain [OF _ dp1 dp2 neq])
 show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by auto
 qed
 lemma dependents_child_unique:
 fixes s th th1 th2 th3
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and ch1: "(Th th1, Th th) \<in> child s"
 and ch2: "(Th th2, Th th) \<in> child s"
 and dp1: "th3 \<in> dependents s th1"
 and dp2: "th3 \<in> dependents s th2"
 shows "th1 = th2"
 } thus ?thesis by auto
 qed
 lemma cp_rec:
 fixes s th
-assumes vt: "vt step s"
+assumes vt: "vt s"
 shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"
 proof(unfold cp_eq_cpreced_f cpreced_def)
 let ?f = "(\<lambda>th. preced th s)"
 show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =
 Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th)"
 where "cps s = {(th, cp s th) | th . th \<in> threads s}"
 locale step_set_cps =
 fixes s' th prio s
 defines s_def : "s \<equiv> (Set th prio#s')"
-assumes vt_s: "vt step s"
+assumes vt_s: "vt s"
 context step_set_cps
 begin
 lemma eq_preced:
 ultimately show ?thesis by auto
 qed
 end
 lemma next_waiting:
-assumes vt: "vt step s"
+assumes vt: "vt s"
 and nxt: "next_th s th cs th'"
 shows "waiting s th' cs"
 proof -
 from assms show ?thesis
-apply (auto simp:next_th_def s_waiting_def)
+apply (auto simp:next_th_def s_waiting_def[folded wq_def])
 proof -
 fix rest
 assume ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> set rest"
 and eq_wq: "wq s cs = th # rest"
 and ne: "rest \<noteq> []"
 qed
 locale step_v_cps =
 fixes s' th cs s
 defines s_def : "s \<equiv> (V th cs#s')"
-assumes vt_s: "vt step s"
+assumes vt_s: "vt s"
 locale step_v_cps_nt = step_v_cps +
 fixes th'
 assumes nt: "next_th s' th cs th'"
 from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (depend s)^+" by auto
 moreover have "cs' = cs"
 proof -
 from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
 have "(Th th', Cs cs) \<in> depend s'"
-by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
 from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']
 show ?thesis by simp
 qed
 ultimately have "(Cs cs, Cs cs) \<in> (depend s)^+" by simp
 moreover note wf_trancl[OF wf_depend[OF vt_s]]
 with depend_s have dps': "(Th th', z) \<in> depend s'" by auto
 have "z = Cs cs"
 proof -
 from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
 have "(Th th', Cs cs) \<in> depend s'"
-by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
 from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]
 show ?thesis .
 qed
 with dps depend_s show False by auto
 qed
 with yz have dp_yz: "(Cs cs, z) \<in> depend s'" by simp
 from this have eq_z: "z = Th th"
 proof -
 from step_back_step[OF vt_s[unfolded s_def]]
 have "(Cs cs, Th th) \<in> depend s'"
-by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+by(cases, auto simp: wq_def s_depend_def cs_holding_def s_holding_def)
 from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this dp_yz]
 show ?thesis by simp
 qed
 from converse_tranclE[OF ztp]
 obtain u where "(z, u) \<in> depend s'" by auto
 moreover
 from step_back_step[OF vt_s[unfolded s_def]]
 have "th \<in> readys s'" by (cases, simp add:runing_def)
 moreover note eq_z
 ultimately show False
-by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
 qed
 next
 show "y \<noteq> Th th'"
 proof
 assume eq_y: "y = Th th'"
 with yz have dps: "(Th th', z) \<in> depend s'" by simp
 have "z = Cs cs"
 proof -
 from next_waiting[OF step_back_vt[OF vt_s[unfolded s_def]] nt]
 have "(Th th', Cs cs) \<in> depend s'"
-by (auto simp:s_waiting_def s_depend_def cs_waiting_def)
+by (auto simp:s_waiting_def wq_def s_depend_def cs_waiting_def)
 from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] dps this]
 show ?thesis .
 qed
 with ztp have cs_i: "(Cs cs, Th th'') \<in>  (depend s')\<^sup>+" by simp
 from step_back_step[OF vt_s[unfolded s_def]]
 have cs_th: "(Cs cs, Th th) \<in> depend s'"
-by(cases, auto simp: s_depend_def cs_holding_def s_holding_def)
+by(cases, auto simp: s_depend_def wq_def cs_holding_def s_holding_def)
 have "(Cs cs, Th th'') \<notin>  depend s'"
 proof
 assume "(Cs cs, Th th'') \<in> depend s'"
 from unique_depend[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]
 and neq1 show "False" by simp
 from converse_tranclE[OF this]
 obtain v where "(Th th, v) \<in> (depend s')" by auto
 moreover from step_back_step[OF vt_s[unfolded s_def]]
 have "th \<in> readys s'" by (cases, simp add:runing_def)
 ultimately show False
-by (auto simp:readys_def s_depend_def s_waiting_def cs_waiting_def)
+by (auto simp:readys_def wq_def s_depend_def s_waiting_def cs_waiting_def)
 qed
 qed
 with depend_s yz have "(y, z) \<in> depend s" by auto
 with ztp'
 show "(y, Th th'') \<in> (depend s)\<^sup>+" by auto
 show "False"
 proof(cases)
 assume "holding s' th cs"
 then obtain rest where
 eq_wq: "wq s' cs = th#rest"
-apply (unfold s_holding_def)
+apply (unfold s_holding_def wq_def[symmetric])
 by (case_tac "(wq s' cs)", auto)
 with h1 h2 have ne: "rest \<noteq> []" by auto
 with eq_wq
 have "next_th s' th cs (hd (SOME q. distinct q \<and> set q = set rest))"
 by(unfold next_th_def, rule_tac x = "rest" in exI, auto)
 end
 locale step_P_cps =
 fixes s' th cs s
 defines s_def : "s \<equiv> (P th cs#s')"
-assumes vt_s: "vt step s"
+assumes vt_s: "vt s"
 locale step_P_cps_ne =step_P_cps +
 assumes ne: "wq s' cs \<noteq> []"
 locale step_P_cps_e =step_P_cps +
 end
 locale step_create_cps =
 fixes s' th prio s
 defines s_def : "s \<equiv> (Create th prio#s')"
-assumes vt_s: "vt step s"
+assumes vt_s: "vt s"
 context step_create_cps
 begin
 lemma eq_dep: "depend s = depend s'"
 locale step_exit_cps =
 fixes s' th prio s
 defines s_def : "s \<equiv> (Exit th#s')"
-assumes vt_s: "vt step s"
+assumes vt_s: "vt s"
 context step_exit_cps
 begin
 lemma eq_dep: "depend s = depend s'"
 show False
 proof(cases)
 assume "th \<in> runing s'"
 with bk show ?thesis
 apply (unfold runing_def readys_def s_waiting_def s_depend_def)
-by (auto simp:cs_waiting_def)
+by (auto simp:cs_waiting_def wq_def)
 qed
 qed
 have eq_dp: "\<And> th. dependents (wq s) th = dependents (wq s') th"
 by (unfold cs_dependents_def, auto simp:eq_dep eq_depend)
 moreover {

changeset 298	f2e0d031a395
parent 290	6a6d0bd16035
child 312	09281ccb31bd