section {*+
−
  This file contains lemmas used to guide the recalculation of current precedence +
−
  after every system call (or system operation)+
−
*}+
−
theory CpsG+
−
imports PrioG Max RTree+
−
begin+
−
+
−
locale pip = +
−
  fixes s+
−
  assumes vt: "vt s"+
−
+
−
context pip+
−
begin+
−
+
−
interpretation rtree_RAG: rtree "RAG s"+
−
proof+
−
  show "single_valued (RAG s)"+
−
  apply (intro_locales)+
−
    by (unfold single_valued_def, auto intro: unique_RAG[OF vt])+
−
+
−
  show "acyclic (RAG s)"+
−
     by (rule acyclic_RAG[OF vt])+
−
qed+
−
+
−
end+
−
+
−
+
−
+
−
definition "the_preced s th = preced th s"+
−
+
−
lemma cp_alt_def:+
−
  "cp s th =  +
−
           Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"+
−
proof -+
−
  have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =+
−
        Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" +
−
          (is "Max (_ ` ?L) = Max (_ ` ?R)")+
−
  proof -+
−
    have "?L = ?R" +
−
    by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)+
−
    thus ?thesis by simp+
−
  qed+
−
  thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)+
−
qed+
−
+
−
lemma eq_dependants: "dependants (wq s) = dependants s"+
−
  by (simp add: s_dependants_abv wq_def)+
−
  +
−
(* obvious lemma *)+
−
lemma not_thread_holdents:+
−
  fixes th 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 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)+
−
      case (thread_create thread prio)+
−
      assume eq_e: "e = Create thread prio"+
−
        and not_in': "thread \<notin> threads s"+
−
      have "holdents (e # s) th = holdents s th"+
−
        apply (unfold eq_e holdents_test)+
−
        by (simp add:RAG_create_unchanged)+
−
      moreover have "th \<notin> threads s" +
−
      proof -+
−
        from not_in eq_e show ?thesis by simp+
−
      qed+
−
      moreover note ih ultimately show ?thesis by auto+
−
    next+
−
      case (thread_exit thread)+
−
      assume eq_e: "e = Exit thread"+
−
      and nh: "holdents s thread = {}"+
−
      show ?thesis+
−
      proof(cases "th = thread")+
−
        case True+
−
        with nh eq_e+
−
        show ?thesis +
−
          by (auto simp:holdents_test RAG_exit_unchanged)+
−
      next+
−
        case False+
−
        with not_in and eq_e+
−
        have "th \<notin> threads s" by simp+
−
        from ih[OF this] False eq_e show ?thesis +
−
          by (auto simp:holdents_test RAG_exit_unchanged)+
−
      qed+
−
    next+
−
      case (thread_P thread cs)+
−
      assume eq_e: "e = P thread cs"+
−
      and is_runing: "thread \<in> runing s"+
−
      from assms thread_exit ih stp not_in vt eq_e 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)+
−
        ultimately show ?thesis by auto+
−
      qed+
−
      hence "holdents (e # s) th  = holdents s th "+
−
        apply (unfold cntCS_def holdents_test eq_e)+
−
        by (unfold step_RAG_p[OF vtp], auto)+
−
      moreover have "holdents s th = {}"+
−
      proof(rule ih)+
−
        from not_in eq_e show "th \<notin> threads s" by simp+
−
      qed+
−
      ultimately show ?thesis by simp+
−
    next+
−
      case (thread_V thread cs)+
−
      assume eq_e: "e = V thread cs"+
−
        and is_runing: "thread \<in> runing s"+
−
        and hold: "holding s thread cs"+
−
      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)+
−
        ultimately show ?thesis by auto+
−
      qed+
−
      from assms thread_V eq_e ih stp not_in vt 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: 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> []"+
−
          and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")+
−
        have "?t \<in> set rest"+
−
        proof(rule someI2)+
−
          from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq+
−
          show "distinct rest \<and> set rest = set rest" by auto+
−
        next+
−
          fix x assume "distinct x \<and> set x = set rest" with ne+
−
          show "hd x \<in> set rest" by (cases x, auto)+
−
        qed+
−
        with eq_wq have "?t \<in> set (wq s cs)" by simp+
−
        from wq_threads[OF step_back_vt[OF vtv], OF this] and ni+
−
        show False by auto+
−
      qed+
−
      moreover note neq_th eq_wq+
−
      ultimately have "holdents (e # s) th  = holdents s th"+
−
        by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)+
−
      moreover have "holdents s th = {}"+
−
      proof(rule ih)+
−
        from not_in eq_e show "th \<notin> threads s" by simp+
−
      qed+
−
      ultimately show ?thesis by simp+
−
    next+
−
      case (thread_set thread prio)+
−
      print_facts+
−
      assume eq_e: "e = Set thread prio"+
−
        and is_runing: "thread \<in> runing s"+
−
      from not_in and eq_e have "th \<notin> threads s" by auto+
−
      from ih [OF this] and eq_e+
−
      show ?thesis +
−
        apply (unfold eq_e cntCS_def holdents_test)+
−
        by (simp add:RAG_set_unchanged)+
−
    qed+
−
    next+
−
      case vt_nil+
−
      show ?case+
−
      by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)+
−
  qed+
−
qed+
−
+
−
(* obvious lemma *)+
−
lemma next_th_neq: +
−
  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)+
−
  proof -+
−
    fix rest+
−
    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"+
−
      and ne: "rest \<noteq> []"+
−
    have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" +
−
    proof(rule someI2)+
−
      from wq_distinct[OF vt, of cs] eq_wq+
−
      show "distinct rest \<and> set rest = set rest" by auto+
−
    next+
−
      fix x+
−
      assume "distinct x \<and> set x = set rest"+
−
      hence eq_set: "set x = set rest" by auto+
−
      with ne have "x \<noteq> []" by auto+
−
      hence "hd x \<in> set x" by auto+
−
      with eq_set show "hd x \<in> set rest" by auto+
−
    qed+
−
    with wq_distinct[OF vt, of cs] eq_wq show False by auto+
−
  qed+
−
qed+
−
+
−
(* obvious lemma *)+
−
lemma next_th_unique: +
−
  assumes nt1: "next_th s th cs th1"+
−
  and nt2: "next_th s th cs th2"+
−
  shows "th1 = th2"+
−
using assms by (unfold next_th_def, auto)+
−
+
−
lemma wf_RAG:+
−
  assumes vt: "vt s"+
−
  shows "wf (RAG s)"+
−
proof(rule finite_acyclic_wf)+
−
  from finite_RAG[OF vt] show "finite (RAG s)" .+
−
next+
−
  from acyclic_RAG[OF vt] show "acyclic (RAG s)" .+
−
qed+
−
+
−
definition child :: "state \<Rightarrow> (node \<times> node) set"+
−
  where "child s \<equiv>+
−
            {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"+
−
+
−
definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"+
−
  where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"+
−
+
−
lemma children_def2:+
−
  "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"+
−
unfolding child_def children_def by simp+
−
+
−
lemma children_dependants: +
−
  "children s th \<subseteq> dependants (wq s) th"+
−
  unfolding children_def2+
−
  unfolding cs_dependants_def+
−
  by (auto simp add: eq_RAG)+
−
+
−
lemma child_unique:+
−
  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"+
−
using ch1 ch2 +
−
proof(unfold child_def, clarsimp)+
−
  fix cs csa+
−
  assume h1: "(Th th, Cs cs) \<in> RAG s"+
−
    and h2: "(Cs cs, Th th1) \<in> RAG s"+
−
    and h3: "(Th th, Cs csa) \<in> RAG s"+
−
    and h4: "(Cs csa, Th th2) \<in> RAG s"+
−
  from unique_RAG[OF vt h1 h3] have "cs = csa" by simp+
−
  with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp+
−
  from unique_RAG[OF vt h2 this]+
−
  show "th1 = th2" by simp+
−
qed +
−
+
−
lemma RAG_children:+
−
  assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"+
−
  shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"+
−
proof -+
−
  from h show ?thesis+
−
  proof(induct rule: tranclE)+
−
    fix c th2+
−
    assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"+
−
    and h2: "(c, Th th2) \<in> RAG s"+
−
    from h2 obtain cs where eq_c: "c = Cs cs"+
−
      by (case_tac c, auto simp:s_RAG_def)+
−
    show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"+
−
    proof(rule tranclE[OF h1])+
−
      fix ca+
−
      assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"+
−
        and h4: "(ca, c) \<in> RAG s"+
−
      show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"+
−
      proof -+
−
        from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"+
−
          by (case_tac ca, auto simp:s_RAG_def)+
−
        from eq_ca h4 h2 eq_c+
−
        have "th3 \<in> children s th2" by (auto simp:children_def child_def)+
−
        moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp+
−
        ultimately show ?thesis by auto+
−
      qed+
−
    next+
−
      assume "(Th th1, c) \<in> RAG s"+
−
      with h2 eq_c+
−
      have "th1 \<in> children s th2"+
−
        by (auto simp:children_def child_def)+
−
      thus ?thesis by auto+
−
    qed+
−
  next+
−
    assume "(Th th1, Th th2) \<in> RAG s"+
−
    thus ?thesis+
−
      by (auto simp:s_RAG_def)+
−
  qed+
−
qed+
−
+
−
lemma sub_child: "child s \<subseteq> (RAG s)^+"+
−
  by (unfold child_def, auto)+
−
+
−
lemma wf_child: +
−
  assumes vt: "vt s"+
−
  shows "wf (child s)"+
−
apply(rule wf_subset)+
−
apply(rule wf_trancl[OF wf_RAG[OF vt]])+
−
apply(rule sub_child)+
−
done+
−
+
−
lemma RAG_child_pre:+
−
  assumes vt: "vt s"+
−
  shows+
−
  "(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")+
−
proof -+
−
  from wf_trancl[OF wf_RAG[OF vt]]+
−
  have wf: "wf ((RAG s)^+)" .+
−
  show ?thesis+
−
  proof(rule wf_induct[OF wf, of ?P], clarsimp)+
−
    fix th'+
−
    assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>+
−
               (Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"+
−
    and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"+
−
    show "(Th th, Th th') \<in> (child s)\<^sup>+"+
−
    proof -+
−
      from RAG_children[OF h]+
−
      have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .+
−
      thus ?thesis+
−
      proof+
−
        assume "th \<in> children s th'"+
−
        thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)+
−
      next+
−
        assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"+
−
        then obtain th3 where th3_in: "th3 \<in> children s th'" +
−
          and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto+
−
        from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)+
−
        from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp+
−
        with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)+
−
      qed+
−
    qed+
−
  qed+
−
qed+
−
+
−
lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"+
−
  by (insert RAG_child_pre, auto)+
−
+
−
lemma child_RAG_p:+
−
  assumes "(n1, n2) \<in> (child s)^+"+
−
  shows "(n1, n2) \<in> (RAG s)^+"+
−
proof -+
−
  from assms show ?thesis+
−
  proof(induct)+
−
    case (base y)+
−
    with sub_child show ?case by auto+
−
  next+
−
    case (step y z)+
−
    assume "(y, z) \<in> child s"+
−
    with sub_child have "(y, z) \<in> (RAG s)^+" by auto+
−
    moreover have "(n1, y) \<in> (RAG s)^+" by fact+
−
    ultimately show ?case by auto+
−
  qed+
−
qed+
−
+
−
text {* (* ddd *)+
−
*}+
−
lemma child_RAG_eq: +
−
  assumes vt: "vt s"+
−
  shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"+
−
  by (auto intro: RAG_child[OF vt] child_RAG_p)+
−
+
−
text {* (* ddd *)+
−
*}+
−
lemma children_no_dep:+
−
  fixes s th th1 th2 th3+
−
  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> (RAG s)^+"+
−
  shows "False"+
−
proof -+
−
  from RAG_child[OF vt ch3]+
−
  have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .+
−
  thus ?thesis+
−
  proof(rule converse_tranclE)+
−
    assume "(Th th1, Th th2) \<in> child s"+
−
    from child_unique[OF vt ch1 this] have "th = th2" by simp+
−
    with ch2 have "(Th th2, Th th2) \<in> child s" by simp+
−
    with wf_child[OF vt] show ?thesis by auto+
−
  next+
−
    fix c+
−
    assume h1: "(Th th1, c) \<in> child s"+
−
      and h2: "(c, Th th2) \<in> (child s)\<^sup>+"+
−
    from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)+
−
    with h1 have "(Th th1, Th th3) \<in> child s" by simp+
−
    from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp+
−
    with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp+
−
    with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto+
−
    moreover have "wf ((child s)\<^sup>+)"+
−
    proof(rule wf_trancl)+
−
      from wf_child[OF vt] show "wf (child s)" .+
−
    qed+
−
    ultimately show False by auto+
−
  qed+
−
qed+
−
+
−
text {* (* ddd *)+
−
*}+
−
lemma unique_RAG_p:+
−
  assumes vt: "vt s"+
−
  and dp1: "(n, n1) \<in> (RAG s)^+"+
−
  and dp2: "(n, n2) \<in> (RAG s)^+"+
−
  and neq: "n1 \<noteq> n2"+
−
  shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"+
−
proof(rule unique_chain [OF _ dp1 dp2 neq])+
−
  from unique_RAG[OF vt]+
−
  show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto+
−
qed+
−
+
−
text {* (* ddd *)+
−
*}+
−
lemma dependants_child_unique:+
−
  fixes s th th1 th2 th3+
−
  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> dependants s th1"+
−
  and dp2: "th3 \<in> dependants s th2"+
−
shows "th1 = th2"+
−
proof -+
−
  { assume neq: "th1 \<noteq> th2"+
−
    from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+" +
−
      by (simp add:s_dependants_def eq_RAG)+
−
    from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+" +
−
      by (simp add:s_dependants_def eq_RAG)+
−
    from unique_RAG_p[OF vt dp1 dp2] and neq+
−
    have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto+
−
    hence False+
−
    proof+
−
      assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ "+
−
      from children_no_dep[OF vt ch1 ch2 this] show ?thesis .+
−
    next+
−
      assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"+
−
      from children_no_dep[OF vt ch2 ch1 this] show ?thesis .+
−
    qed+
−
  } thus ?thesis by auto+
−
qed+
−
+
−
lemma RAG_plus_elim:+
−
  assumes "vt s"+
−
  fixes x+
−
  assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"+
−
  shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"+
−
  using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]+
−
  apply (unfold children_def)+
−
  by (metis assms(2) children_def RAG_children eq_RAG)+
−
+
−
text {* (* ddd *)+
−
*}+
−
lemma dependants_expand:+
−
  assumes "vt s"+
−
  shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"+
−
apply(simp add: image_def)+
−
unfolding cs_dependants_def+
−
apply(auto)+
−
apply (metis assms RAG_plus_elim mem_Collect_eq)+
−
apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')+
−
by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)+
−
+
−
lemma finite_children:+
−
  assumes "vt s"+
−
  shows "finite (children s th)"+
−
  using children_dependants dependants_threads[OF assms] finite_threads[OF assms]+
−
  by (metis rev_finite_subset)+
−
  +
−
lemma finite_dependants:+
−
  assumes "vt s"+
−
  shows "finite (dependants (wq s) th')"+
−
  using dependants_threads[OF assms] finite_threads[OF assms]+
−
  by (metis rev_finite_subset)+
−
+
−
abbreviation+
−
  "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"+
−
+
−
abbreviation+
−
  "cpreceds s ths \<equiv> (cp s) ` ths"+
−
+
−
lemma Un_compr:+
−
  "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"+
−
by auto+
−
+
−
lemma in_disj:+
−
  shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"+
−
by metis+
−
+
−
lemma UN_exists:+
−
  shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"+
−
by auto+
−
+
−
text {* (* ddd *)+
−
  This is the recursive equation used to compute the current precedence of +
−
  a thread (the @{text "th"}) here. +
−
*}+
−
lemma cp_rec:+
−
  fixes s th+
−
  assumes vt: "vt s"+
−
  shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"+
−
proof(cases "children s th = {}")+
−
  case True+
−
  show ?thesis+
−
    unfolding cp_eq_cpreced cpreced_def +
−
    by (subst dependants_expand[OF `vt s`]) (simp add: True)+
−
next+
−
  case False+
−
  show ?thesis (is "?LHS = ?RHS")+
−
  proof -+
−
    have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"+
−
      by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])+
−
  +
−
    have not_emptyness_facts[simp]: +
−
      "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"+
−
      using False dependants_expand[OF assms] by(auto simp only: Un_empty)+
−
+
−
    have finiteness_facts[simp]:+
−
      "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"+
−
      by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])+
−
+
−
    (* expanding definition *)+
−
    have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"+
−
      unfolding eq_cp by (simp add: Un_compr)+
−
    +
−
    (* moving Max in *)+
−
    also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"+
−
      by (simp add: Max_Un)+
−
+
−
    (* expanding dependants *)+
−
    also have "\<dots> = max (Max {preced th s}) +
−
      (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"+
−
      by (subst dependants_expand[OF `vt s`]) (simp)+
−
+
−
    (* moving out big Union *)+
−
    also have "\<dots> = max (Max {preced th s})+
−
      (Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"  +
−
      by simp+
−
+
−
    (* moving in small union *)+
−
    also have "\<dots> = max (Max {preced th s})+
−
      (Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"  +
−
      by (simp add: in_disj)+
−
+
−
    (* moving in preceds *)+
−
    also have "\<dots> = max (Max {preced th s})  +
−
      (Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))" +
−
      by (simp add: UN_exists)+
−
+
−
    (* moving in Max *)+
−
    also have "\<dots> = max (Max {preced th s})  +
−
      (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))" +
−
      by (subst Max_Union) (auto simp add: image_image)+
−
+
−
    (* folding cp + moving out Max *)+
−
    also have "\<dots> = ?RHS" +
−
      unfolding eq_cp by (simp add: Max_insert)+
−
+
−
    finally show "?LHS = ?RHS" .+
−
  qed+
−
qed+
−
+
−
lemma next_waiting:+
−
  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[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> []"+
−
    have "set (SOME q. distinct q \<and> set q = set rest) = set rest" +
−
    proof(rule someI2)+
−
      from wq_distinct[OF vt, of cs] eq_wq+
−
      show "distinct rest \<and> set rest = set rest" by auto+
−
    next+
−
      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto+
−
    qed+
−
    with ni+
−
    have "hd (SOME q. distinct q \<and> set q = set rest) \<notin>  set (SOME q. distinct q \<and> set q = set rest)"+
−
      by simp+
−
    moreover have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"+
−
    proof(rule someI2)+
−
      from wq_distinct[OF vt, of cs] eq_wq+
−
      show "distinct rest \<and> set rest = set rest" by auto+
−
    next+
−
      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto+
−
    qed+
−
    ultimately show "hd (SOME q. distinct q \<and> set q = set rest) = th" by auto+
−
  next+
−
    fix rest+
−
    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"+
−
      and ne: "rest \<noteq> []"+
−
    have "(SOME q. distinct q \<and> set q = set rest) \<noteq> []"+
−
    proof(rule someI2)+
−
      from wq_distinct[OF vt, of cs] eq_wq+
−
      show "distinct rest \<and> set rest = set rest" by auto+
−
    next+
−
      from ne show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> x \<noteq> []" by auto+
−
    qed+
−
    hence "hd (SOME q. distinct q \<and> set q = set rest) \<in> set (SOME q. distinct q \<and> set q = set rest)"+
−
      by auto+
−
    moreover have "set (SOME q. distinct q \<and> set q = set rest) = set rest" +
−
    proof(rule someI2)+
−
      from wq_distinct[OF vt, of cs] eq_wq+
−
      show "distinct rest \<and> set rest = set rest" by auto+
−
    next+
−
      show "\<And>x. distinct x \<and> set x = set rest \<Longrightarrow> set x = set rest" by auto+
−
    qed+
−
    ultimately have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" by simp+
−
    with eq_wq and wq_distinct[OF vt, of cs]+
−
    show False by auto+
−
  qed+
−
qed+
−
+
−
-- {* A useless definition *}+
−
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"+
−
where "cps s = {(th, cp s th) | th . th \<in> threads s}"+
−
+
−
+
−
text {* (* ddd *)+
−
  One beauty of our modelling is that we follow the definitional extension tradition of HOL.+
−
  The benefit of such a concise and miniature model is that  large number of intuitively +
−
  obvious facts are derived as lemmas, rather than asserted as axioms.+
−
*}+
−
+
−
text {*+
−
  However, the lemmas in the forthcoming several locales are no longer +
−
  obvious. These lemmas show how the current precedences should be recalculated +
−
  after every execution step (in our model, every step is represented by an event, +
−
  which in turn, represents a system call, or operation). Each operation is +
−
  treated in a separate locale.+
−
+
−
  The complication of current precedence recalculation comes +
−
  because the changing of RAG needs to be taken into account, +
−
  in addition to the changing of precedence. +
−
  The reason RAG changing affects current precedence is that,+
−
  according to the definition, current precedence +
−
  of a thread is the maximum of the precedences of its dependants, +
−
  where the dependants are defined in terms of RAG.+
−
+
−
  Therefore, each operation, lemmas concerning the change of the precedences +
−
  and RAG are derived first, so that the lemmas about+
−
  current precedence recalculation can be based on.+
−
*}+
−
+
−
text {* (* ddd *)+
−
  The following locale @{text "step_set_cps"} investigates the recalculation +
−
  after the @{text "Set"} operation.+
−
*}+
−
locale step_set_cps =+
−
  fixes s' th prio s +
−
  -- {* @{text "s'"} is the system state before the operation *}+
−
  -- {* @{text "s"} is the system state after the operation *}+
−
  defines s_def : "s \<equiv> (Set th prio#s')" +
−
  -- {* @{text "s"} is assumed to be a legitimate state, from which+
−
         the legitimacy of @{text "s"} can be derived. *}+
−
  assumes vt_s: "vt s"+
−
+
−
context step_set_cps +
−
begin+
−
+
−
interpretation rtree_RAGs: rtree "RAG s"+
−
proof+
−
  show "single_valued (RAG s)"+
−
  apply (intro_locales)+
−
    by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])+
−
+
−
  show "acyclic (RAG s)"+
−
     by (rule acyclic_RAG[OF vt_s])+
−
qed+
−
+
−
interpretation rtree_RAGs': rtree "RAG s'"+
−
proof+
−
  show "single_valued (RAG s')"+
−
  apply (intro_locales)+
−
    by (unfold single_valued_def, +
−
        auto intro: unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])+
−
+
−
  show "acyclic (RAG s')"+
−
     by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])+
−
qed+
−
+
−
text {* (* ddd *)+
−
  The following lemma confirms that @{text "Set"}-operating only changes the precedence +
−
  of initiating thread.+
−
*}+
−
+
−
lemma eq_preced:+
−
  fixes th'+
−
  assumes "th' \<noteq> th"+
−
  shows "preced th' s = preced th' s'"+
−
proof -+
−
  from assms show ?thesis +
−
    by (unfold s_def, auto simp:preced_def)+
−
qed+
−
+
−
text {* (* ddd *)+
−
  The following lemma assures that the resetting of priority does not change the RAG. +
−
*}+
−
+
−
lemma eq_dep: "RAG s = RAG s'"+
−
  by (unfold s_def RAG_set_unchanged, auto)+
−
+
−
text {*+
−
  Th following lemma @{text "eq_cp_pre"} circumscribe a rough range of recalculation.+
−
  It says, thread other than the initiating thread @{text "th"} does not need recalculation+
−
  unless it lies upstream of @{text "th"} in the RAG. +
−
+
−
  The reason behind this lemma is that: +
−
  the change of precedence of one thread can only affect it's upstream threads, according to +
−
  lemma @{text "eq_preced"}. Since the only thread which might change precedence is+
−
  @{text "th"}, so only @{text "th"} and its upstream threads need recalculation.+
−
  (* ccc *)+
−
*}+
−
+
−
lemma eq_cp_pre:+
−
  fixes th' +
−
  assumes neq_th: "th' \<noteq> th"+
−
  and nd: "th \<notin> dependants s th'"+
−
  shows "cp s th' = cp s' th'"+
−
proof -+
−
  -- {* This is what we need to prove after expanding the definition of @{text "cp"} *}+
−
  have "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =+
−
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))"+
−
   (is "Max (?f1 ` ({th'} \<union> ?A)) = Max (?f2 ` ({th'} \<union> ?B))") +
−
  proof -+
−
      -- {* Since RAG is not changed by @{text "Set"}-operation, the dependants of +
−
            any threads are not changed, this is one of key facts underpinning this +
−
            lemma *}+
−
      have eq_ab: "?A = ?B" by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)+
−
      have "(?f1 ` ({th'} \<union> ?A)) =  (?f2 ` ({th'} \<union> ?B))"+
−
      proof(rule image_cong)+
−
        show "{th'} \<union> ?A = {th'} \<union> ?B" by (simp only:eq_ab)+
−
      next  +
−
        fix x+
−
        assume x_in: "x \<in> {th'} \<union> ?B"+
−
        show "?f1 x = ?f2 x"+
−
        proof(rule eq_preced) -- {* The other key fact underpinning this lemma is @{text "eq_preced"} *}+
−
          from x_in[folded eq_ab, unfolded eq_dependants]+
−
          have "x \<in> {th'} \<union> dependants s th'" .+
−
          thus "x \<noteq> th"+
−
          proof+
−
            assume "x \<in> {th'}" +
−
            with `th' \<noteq> th` show ?thesis by simp+
−
          next+
−
            assume "x \<in> dependants s th'"+
−
            with `th \<notin> dependants s th'` show ?thesis by auto+
−
          qed +
−
        qed +
−
      qed+
−
      thus ?thesis by simp+
−
  qed +
−
  thus ?thesis by (unfold cp_eq_cpreced cpreced_def)+
−
qed+
−
+
−
text {*+
−
  The following lemma shows that no thread lies upstream of the initiating thread @{text "th"}. +
−
  The reason for this is that only no-blocked thread can initiate +
−
  a system call. Since thread @{text "th"} is non-blocked, it is not waiting for any +
−
  critical resource. Therefore, there is edge leading out of @{text "th"} in the RAG.+
−
  Consequently, there is no node (neither resource nor thread) upstream of @{text "th"}.+
−
*}+
−
lemma no_dependants:+
−
  shows "th \<notin> dependants s th'"+
−
proof+
−
  assume "th \<in> dependants s th'"+
−
  from `th \<in> dependants s th'` have "(Th th, Th th') \<in> (RAG s')\<^sup>+"+
−
    by (unfold s_dependants_def, unfold eq_RAG, unfold eq_dep, auto)+
−
  from tranclD[OF this]+
−
  obtain z where "(Th th, z) \<in> RAG s'" by auto+
−
  moreover have "th \<in> readys s'"+
−
  proof -+
−
    from step_back_step [OF vt_s[unfolded s_def]]+
−
    have "step s' (Set th prio)" .+
−
    hence "th \<in> runing s'" by (cases, simp)+
−
    thus ?thesis by (simp add:readys_def runing_def)+
−
  qed+
−
  ultimately show "False"+
−
    apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)+
−
    by (fold wq_def, blast)+
−
qed+
−
+
−
(* Result improved *)+
−
text {* +
−
  A simple combination of @{text "eq_cp_pre"} and @{text "no_dependants"}+
−
  gives the main lemma of this locale, which shows that+
−
  only the initiating thread needs a recalculation of current precedence.+
−
*}+
−
lemma eq_cp:+
−
  fixes th' +
−
  assumes "th' \<noteq> th"+
−
  shows "cp s th' = cp s' th'"+
−
  by (rule eq_cp_pre[OF assms no_dependants])+
−
+
−
end+
−
+
−
text {*+
−
  The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.+
−
*}+
−
+
−
locale step_v_cps =+
−
  -- {* @{text "th"} is the initiating thread *}+
−
  -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}+
−
  fixes s' th cs s    -- {* @{text "s'"} is the state before operation*}+
−
  defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}+
−
  -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}+
−
  assumes vt_s: "vt s"+
−
+
−
text {*+
−
  The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, +
−
  which represents the case when there is another thread @{text "th'"}+
−
  to take over the critical resource released by the initiating thread @{text "th"}.+
−
*}+
−
locale step_v_cps_nt = step_v_cps ++
−
  fixes th'+
−
  -- {* @{text "th'"} is assumed to take over @{text "cs"} *}+
−
  assumes nt: "next_th s' th cs th'" +
−
+
−
context step_v_cps_nt+
−
begin+
−
+
−
text {*+
−
  Lemma @{text "RAG_s"} confirms the change of RAG:+
−
  two edges removed and one added, as shown by the following diagram.+
−
*}+
−
+
−
(*+
−
  RAG before the V-operation+
−
    th1 ----|+
−
            |+
−
    th' ----|+
−
            |----> cs -----|+
−
    th2 ----|              |+
−
            |              |+
−
    th3 ----|              |+
−
                           |------> th+
−
    th4 ----|              |+
−
            |              |+
−
    th5 ----|              |+
−
            |----> cs'-----|+
−
    th6 ----|+
−
            |+
−
    th7 ----|+
−
+
−
 RAG after the V-operation+
−
    th1 ----|+
−
            |+
−
            |----> cs ----> th'+
−
    th2 ----|              +
−
            |              +
−
    th3 ----|              +
−
                           +
−
    th4 ----|              +
−
            |              +
−
    th5 ----|              +
−
            |----> cs'----> th+
−
    th6 ----|+
−
            |+
−
    th7 ----|+
−
*)+
−
+
−
lemma RAG_s:+
−
  "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>+
−
                                         {(Cs cs, Th th')}"+
−
proof -+
−
  from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]+
−
    and nt show ?thesis  by (auto intro:next_th_unique)+
−
qed+
−
+
−
text {*+
−
  Lemma @{text "dependants_kept"} shows only @{text "th"} and @{text "th'"}+
−
  have their dependants changed.+
−
*}+
−
lemma dependants_kept:+
−
  fixes th''+
−
  assumes neq1: "th'' \<noteq> th"+
−
  and neq2: "th'' \<noteq> th'"+
−
  shows "dependants (wq s) th'' = dependants (wq s') th''"+
−
proof(auto) (* ccc *)+
−
  fix x+
−
  assume "x \<in> dependants (wq s) th''"+
−
  hence dp: "(Th x, Th th'') \<in> (RAG s)^+"+
−
    by (auto simp:cs_dependants_def eq_RAG)+
−
  { fix n+
−
    have "(n, Th th'') \<in> (RAG s)^+ \<Longrightarrow>  (n, Th th'') \<in> (RAG s')^+"+
−
    proof(induct rule:converse_trancl_induct)+
−
      fix y +
−
      assume "(y, Th th'') \<in> RAG s"+
−
      with RAG_s neq1 neq2+
−
      have "(y, Th th'') \<in> RAG s'" by auto+
−
      thus "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto+
−
    next+
−
      fix y z +
−
      assume yz: "(y, z) \<in> RAG s"+
−
        and ztp: "(z, Th th'') \<in> (RAG s)\<^sup>+"+
−
        and ztp': "(z, Th th'') \<in> (RAG s')\<^sup>+"+
−
      have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"+
−
      proof+
−
        show "y \<noteq> Cs cs"+
−
        proof+
−
          assume eq_y: "y = Cs cs"+
−
          with yz have dp_yz: "(Cs cs, z) \<in> RAG s" by simp+
−
          from RAG_s+
−
          have cst': "(Cs cs, Th th') \<in> RAG s" by simp+
−
          from unique_RAG[OF vt_s this dp_yz] +
−
          have eq_z: "z = Th th'" by simp+
−
          with ztp have "(Th th', Th th'') \<in> (RAG s)^+" by simp+
−
          from converse_tranclE[OF this]+
−
          obtain cs' where dp'': "(Th th', Cs cs') \<in> RAG s"+
−
            by (auto simp:s_RAG_def)+
−
          with RAG_s have dp': "(Th th', Cs cs') \<in> RAG s'" by auto+
−
          from dp'' eq_y yz eq_z have "(Cs cs, Cs cs') \<in> (RAG 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> RAG s'"+
−
              by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)+
−
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this dp']+
−
            show ?thesis by simp+
−
          qed+
−
          ultimately have "(Cs cs, Cs cs) \<in> (RAG s)^+" by simp+
−
          moreover note wf_trancl[OF wf_RAG[OF vt_s]]+
−
          ultimately show False by auto+
−
        qed+
−
      next+
−
        show "y \<noteq> Th th'"+
−
        proof+
−
          assume eq_y: "y = Th th'"+
−
          with yz have dps: "(Th th', z) \<in> RAG s" by simp+
−
          with RAG_s have dps': "(Th th', z) \<in> RAG 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> RAG s'"+
−
              by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)+
−
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] dps' this]+
−
            show ?thesis .+
−
          qed+
−
          with dps RAG_s show False by auto+
−
        qed+
−
      qed+
−
      with RAG_s yz have "(y, z) \<in> RAG s'" by auto+
−
      with ztp'+
−
      show "(y, Th th'') \<in> (RAG s')\<^sup>+" by auto+
−
    qed    +
−
  }+
−
  from this[OF dp]+
−
  show "x \<in> dependants (wq s') th''" +
−
    by (auto simp:cs_dependants_def eq_RAG)+
−
next+
−
  fix x+
−
  assume "x \<in> dependants (wq s') th''"+
−
  hence dp: "(Th x, Th th'') \<in> (RAG s')^+"+
−
    by (auto simp:cs_dependants_def eq_RAG)+
−
  { fix n+
−
    have "(n, Th th'') \<in> (RAG s')^+ \<Longrightarrow>  (n, Th th'') \<in> (RAG s)^+"+
−
    proof(induct rule:converse_trancl_induct)+
−
      fix y +
−
      assume "(y, Th th'') \<in> RAG s'"+
−
      with RAG_s neq1 neq2+
−
      have "(y, Th th'') \<in> RAG s" by auto+
−
      thus "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto+
−
    next+
−
      fix y z +
−
      assume yz: "(y, z) \<in> RAG s'"+
−
        and ztp: "(z, Th th'') \<in> (RAG s')\<^sup>+"+
−
        and ztp': "(z, Th th'') \<in> (RAG s)\<^sup>+"+
−
      have "y \<noteq> Cs cs \<and> y \<noteq> Th th'"+
−
      proof+
−
        show "y \<noteq> Cs cs"+
−
        proof+
−
          assume eq_y: "y = Cs cs"+
−
          with yz have dp_yz: "(Cs cs, z) \<in> RAG 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> RAG s'"+
−
              by(cases, auto simp: wq_def s_RAG_def cs_holding_def s_holding_def)+
−
            from unique_RAG[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> RAG 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 wq_def s_RAG_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> RAG 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> RAG s'"+
−
              by (auto simp:s_waiting_def wq_def s_RAG_def cs_waiting_def)+
−
            from unique_RAG[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>  (RAG s')\<^sup>+" by simp+
−
          from step_back_step[OF vt_s[unfolded s_def]]+
−
          have cs_th: "(Cs cs, Th th) \<in> RAG s'"+
−
            by(cases, auto simp: s_RAG_def wq_def cs_holding_def s_holding_def)+
−
          have "(Cs cs, Th th'') \<notin>  RAG s'"+
−
          proof+
−
            assume "(Cs cs, Th th'') \<in> RAG s'"+
−
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] this cs_th]+
−
            and neq1 show "False" by simp+
−
          qed+
−
          with converse_tranclE[OF cs_i]+
−
          obtain u where cu: "(Cs cs, u) \<in> RAG s'"  +
−
            and u_t: "(u, Th th'') \<in> (RAG s')\<^sup>+" by auto+
−
          have "u = Th th"+
−
          proof -+
−
            from unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]] cu cs_th]+
−
            show ?thesis .+
−
          qed+
−
          with u_t have "(Th th, Th th'') \<in> (RAG s')\<^sup>+" by simp+
−
          from converse_tranclE[OF this]+
−
          obtain v where "(Th th, v) \<in> (RAG 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 wq_def s_RAG_def s_waiting_def cs_waiting_def)+
−
        qed+
−
      qed+
−
      with RAG_s yz have "(y, z) \<in> RAG s" by auto+
−
      with ztp'+
−
      show "(y, Th th'') \<in> (RAG s)\<^sup>+" by auto+
−
    qed    +
−
  }+
−
  from this[OF dp]+
−
  show "x \<in> dependants (wq s) th''"+
−
    by (auto simp:cs_dependants_def eq_RAG)+
−
qed+
−
+
−
lemma cp_kept:+
−
  fixes th''+
−
  assumes neq1: "th'' \<noteq> th"+
−
  and neq2: "th'' \<noteq> th'"+
−
  shows "cp s th'' = cp s' th''"+
−
proof -+
−
  from dependants_kept[OF neq1 neq2]+
−
  have "dependants (wq s) th'' = dependants (wq s') th''" .+
−
  moreover {+
−
    fix th1+
−
    assume "th1 \<in> dependants (wq s) th''"+
−
    have "preced th1 s = preced th1 s'" +
−
      by (unfold s_def, auto simp:preced_def)+
−
  }+
−
  moreover have "preced th'' s = preced th'' s'" +
−
    by (unfold s_def, auto simp:preced_def)+
−
  ultimately have "((\<lambda>th. preced th s) ` ({th''} \<union> dependants (wq s) th'')) = +
−
    ((\<lambda>th. preced th s') ` ({th''} \<union> dependants (wq s') th''))"+
−
    by (auto simp:image_def)+
−
  thus ?thesis+
−
    by (unfold cp_eq_cpreced cpreced_def, simp)+
−
qed+
−
+
−
end+
−
+
−
locale step_v_cps_nnt = step_v_cps ++
−
  assumes nnt: "\<And> th'. (\<not> next_th s' th cs th')"+
−
+
−
context step_v_cps_nnt+
−
begin+
−
+
−
lemma nw_cs: "(Th th1, Cs cs) \<notin> RAG s'"+
−
proof+
−
  assume "(Th th1, Cs cs) \<in> RAG s'"+
−
  thus "False"+
−
    apply (auto simp:s_RAG_def cs_waiting_def)+
−
  proof -+
−
    assume h1: "th1 \<in> set (wq s' cs)"+
−
      and h2: "th1 \<noteq> hd (wq s' cs)"+
−
    from step_back_step[OF vt_s[unfolded s_def]]+
−
    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 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)+
−
      with nnt show ?thesis by auto+
−
    qed+
−
  qed+
−
qed+
−
+
−
lemma RAG_s: "RAG s = RAG s' - {(Cs cs, Th th)}"+
−
proof -+
−
  from nnt and  step_RAG_v[OF vt_s[unfolded s_def], folded s_def]+
−
  show ?thesis by auto+
−
qed+
−
+
−
lemma child_kept_left:+
−
  assumes +
−
  "(n1, n2) \<in> (child s')^+"+
−
  shows "(n1, n2) \<in> (child s)^+"+
−
proof -+
−
  from assms show ?thesis +
−
  proof(induct rule: converse_trancl_induct)+
−
    case (base y)+
−
    from base obtain th1 cs1 th2+
−
      where h1: "(Th th1, Cs cs1) \<in> RAG s'"+
−
      and h2: "(Cs cs1, Th th2) \<in> RAG s'"+
−
      and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)+
−
    have "cs1 \<noteq> cs"+
−
    proof+
−
      assume eq_cs: "cs1 = cs"+
−
      with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp+
−
      with nw_cs eq_cs show False by auto+
−
    qed+
−
    with h1 h2 RAG_s have +
−
      h1': "(Th th1, Cs cs1) \<in> RAG s" and+
−
      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto+
−
    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)+
−
    with eq_y eq_n2 have "(y, n2) \<in> child s" by simp+
−
    thus ?case by auto+
−
  next+
−
    case (step y z)+
−
    have "(y, z) \<in> child s'" by fact+
−
    then obtain th1 cs1 th2+
−
      where h1: "(Th th1, Cs cs1) \<in> RAG s'"+
−
      and h2: "(Cs cs1, Th th2) \<in> RAG s'"+
−
      and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)+
−
    have "cs1 \<noteq> cs"+
−
    proof+
−
      assume eq_cs: "cs1 = cs"+
−
      with h1 have "(Th th1, Cs cs1) \<in> RAG s'" by simp+
−
      with nw_cs eq_cs show False by auto+
−
    qed+
−
    with h1 h2 RAG_s have +
−
      h1': "(Th th1, Cs cs1) \<in> RAG s" and+
−
      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto+
−
    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)+
−
    with eq_y eq_z have "(y, z) \<in> child s" by simp+
−
    moreover have "(z, n2) \<in> (child s)^+" by fact+
−
    ultimately show ?case by auto+
−
  qed+
−
qed+
−
+
−
lemma  child_kept_right:+
−
  assumes+
−
  "(n1, n2) \<in> (child s)^+"+
−
  shows "(n1, n2) \<in> (child s')^+"+
−
proof -+
−
  from assms show ?thesis+
−
  proof(induct)+
−
    case (base y)+
−
    from base and RAG_s +
−
    have "(n1, y) \<in> child s'"+
−
      by (auto simp:child_def)+
−
    thus ?case by auto+
−
  next+
−
    case (step y z)+
−
    have "(y, z) \<in> child s" by fact+
−
    with RAG_s have "(y, z) \<in> child s'"+
−
      by (auto simp:child_def)+
−
    moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact+
−
    ultimately show ?case by auto+
−
  qed+
−
qed+
−
+
−
lemma eq_child: "(child s)^+ = (child s')^+"+
−
  by (insert child_kept_left child_kept_right, auto)+
−
+
−
lemma eq_cp:+
−
  fixes th' +
−
  shows "cp s th' = cp s' th'"+
−
  apply (unfold cp_eq_cpreced cpreced_def)+
−
proof -+
−
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"+
−
    apply (unfold cs_dependants_def, unfold eq_RAG)+
−
  proof -+
−
    from eq_child+
−
    have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"+
−
      by simp+
−
    with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]+
−
    show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}"+
−
      by simp+
−
  qed+
−
  moreover {+
−
    fix th1 +
−
    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"+
−
    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto+
−
    hence "preced th1 s = preced th1 s'"+
−
    proof+
−
      assume "th1 = th'"+
−
      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)+
−
    next+
−
      assume "th1 \<in> dependants (wq s') th'"+
−
      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)+
−
    qed+
−
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = +
−
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" +
−
    by (auto simp:image_def)+
−
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =+
−
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp+
−
qed+
−
+
−
end+
−
+
−
locale step_P_cps =+
−
  fixes s' th cs s +
−
  defines s_def : "s \<equiv> (P th cs#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 ++
−
  assumes ee: "wq s' cs = []"+
−
+
−
context step_P_cps_e+
−
begin+
−
+
−
lemma RAG_s: "RAG s = RAG s' \<union> {(Cs cs, Th th)}"+
−
proof -+
−
  from ee and  step_RAG_p[OF vt_s[unfolded s_def], folded s_def]+
−
  show ?thesis by auto+
−
qed+
−
+
−
lemma child_kept_left:+
−
  assumes +
−
  "(n1, n2) \<in> (child s')^+"+
−
  shows "(n1, n2) \<in> (child s)^+"+
−
proof -+
−
  from assms show ?thesis +
−
  proof(induct rule: converse_trancl_induct)+
−
    case (base y)+
−
    from base obtain th1 cs1 th2+
−
      where h1: "(Th th1, Cs cs1) \<in> RAG s'"+
−
      and h2: "(Cs cs1, Th th2) \<in> RAG s'"+
−
      and eq_y: "y = Th th1" and eq_n2: "n2 = Th th2"  by (auto simp:child_def)+
−
    have "cs1 \<noteq> cs"+
−
    proof+
−
      assume eq_cs: "cs1 = cs"+
−
      with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp+
−
      with ee show False+
−
        by (auto simp:s_RAG_def cs_waiting_def)+
−
    qed+
−
    with h1 h2 RAG_s have +
−
      h1': "(Th th1, Cs cs1) \<in> RAG s" and+
−
      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto+
−
    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)+
−
    with eq_y eq_n2 have "(y, n2) \<in> child s" by simp+
−
    thus ?case by auto+
−
  next+
−
    case (step y z)+
−
    have "(y, z) \<in> child s'" by fact+
−
    then obtain th1 cs1 th2+
−
      where h1: "(Th th1, Cs cs1) \<in> RAG s'"+
−
      and h2: "(Cs cs1, Th th2) \<in> RAG s'"+
−
      and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)+
−
    have "cs1 \<noteq> cs"+
−
    proof+
−
      assume eq_cs: "cs1 = cs"+
−
      with h1 have "(Th th1, Cs cs) \<in> RAG s'" by simp+
−
      with ee show False +
−
        by (auto simp:s_RAG_def cs_waiting_def)+
−
    qed+
−
    with h1 h2 RAG_s have +
−
      h1': "(Th th1, Cs cs1) \<in> RAG s" and+
−
      h2': "(Cs cs1, Th th2) \<in> RAG s" by auto+
−
    hence "(Th th1, Th th2) \<in> child s" by (auto simp:child_def)+
−
    with eq_y eq_z have "(y, z) \<in> child s" by simp+
−
    moreover have "(z, n2) \<in> (child s)^+" by fact+
−
    ultimately show ?case by auto+
−
  qed+
−
qed+
−
+
−
lemma  child_kept_right:+
−
  assumes+
−
  "(n1, n2) \<in> (child s)^+"+
−
  shows "(n1, n2) \<in> (child s')^+"+
−
proof -+
−
  from assms show ?thesis+
−
  proof(induct)+
−
    case (base y)+
−
    from base and RAG_s+
−
    have "(n1, y) \<in> child s'"+
−
      apply (auto simp:child_def)+
−
      proof -+
−
        fix th'+
−
        assume "(Th th', Cs cs) \<in> RAG s'"+
−
        with ee have "False"+
−
          by (auto simp:s_RAG_def cs_waiting_def)+
−
        thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto +
−
      qed+
−
    thus ?case by auto+
−
  next+
−
    case (step y z)+
−
    have "(y, z) \<in> child s" by fact+
−
    with RAG_s have "(y, z) \<in> child s'"+
−
      apply (auto simp:child_def)+
−
      proof -+
−
        fix th'+
−
        assume "(Th th', Cs cs) \<in> RAG s'"+
−
        with ee have "False"+
−
          by (auto simp:s_RAG_def cs_waiting_def)+
−
        thus "\<exists>cs. (Th th', Cs cs) \<in> RAG s' \<and> (Cs cs, Th th) \<in> RAG s'" by auto +
−
      qed+
−
    moreover have "(n1, y) \<in> (child s')\<^sup>+" by fact+
−
    ultimately show ?case by auto+
−
  qed+
−
qed+
−
+
−
lemma eq_child: "(child s)^+ = (child s')^+"+
−
  by (insert child_kept_left child_kept_right, auto)+
−
+
−
lemma eq_cp:+
−
  fixes th' +
−
  shows "cp s th' = cp s' th'"+
−
  apply (unfold cp_eq_cpreced cpreced_def)+
−
proof -+
−
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"+
−
    apply (unfold cs_dependants_def, unfold eq_RAG)+
−
  proof -+
−
    from eq_child+
−
    have "\<And>th. {th'. (Th th', Th th) \<in> (child s)\<^sup>+} = {th'. (Th th', Th th) \<in> (child s')\<^sup>+}"+
−
      by auto+
−
    with child_RAG_eq[OF vt_s] child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]+
−
    show "\<And>th. {th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} = {th'. (Th th', Th th) \<in> (RAG s')\<^sup>+}"+
−
      by simp+
−
  qed+
−
  moreover {+
−
    fix th1 +
−
    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"+
−
    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto+
−
    hence "preced th1 s = preced th1 s'"+
−
    proof+
−
      assume "th1 = th'"+
−
      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)+
−
    next+
−
      assume "th1 \<in> dependants (wq s') th'"+
−
      show "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)+
−
    qed+
−
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = +
−
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" +
−
    by (auto simp:image_def)+
−
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =+
−
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp+
−
qed+
−
+
−
end+
−
+
−
context step_P_cps_ne+
−
begin+
−
+
−
lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"+
−
proof -+
−
  from step_RAG_p[OF vt_s[unfolded s_def]] and ne+
−
  show ?thesis by (simp add:s_def)+
−
qed+
−
+
−
+
−
lemma eq_child_left:+
−
  assumes nd: "(Th th, Th th') \<notin> (child s)^+"+
−
  shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"+
−
proof(induct rule:converse_trancl_induct)+
−
  case (base y)+
−
  from base obtain th1 cs1+
−
    where h1: "(Th th1, Cs cs1) \<in> RAG s"+
−
    and h2: "(Cs cs1, Th th') \<in> RAG s"+
−
    and eq_y: "y = Th th1"   by (auto simp:child_def)+
−
  have "th1 \<noteq> th"+
−
  proof+
−
    assume "th1 = th"+
−
    with base eq_y have "(Th th, Th th') \<in> child s" by simp+
−
    with nd show False by auto+
−
  qed+
−
  with h1 h2 RAG_s +
−
  have h1': "(Th th1, Cs cs1) \<in> RAG s'" and +
−
       h2': "(Cs cs1, Th th') \<in> RAG s'" by auto+
−
  with eq_y show ?case by (auto simp:child_def)+
−
next+
−
  case (step y z)+
−
  have yz: "(y, z) \<in> child s" by fact+
−
  then obtain th1 cs1 th2+
−
    where h1: "(Th th1, Cs cs1) \<in> RAG s"+
−
    and h2: "(Cs cs1, Th th2) \<in> RAG s"+
−
    and eq_y: "y = Th th1" and eq_z: "z = Th th2"  by (auto simp:child_def)+
−
  have "th1 \<noteq> th"+
−
  proof+
−
    assume "th1 = th"+
−
    with yz eq_y have "(Th th, z) \<in> child s" by simp+
−
    moreover have "(z, Th th') \<in> (child s)^+" by fact+
−
    ultimately have "(Th th, Th th') \<in> (child s)^+" by auto+
−
    with nd show False by auto+
−
  qed+
−
  with h1 h2 RAG_s have h1': "(Th th1, Cs cs1) \<in> RAG s'"+
−
                       and h2': "(Cs cs1, Th th2) \<in> RAG s'" by auto+
−
  with eq_y eq_z have "(y, z) \<in> child s'" by (auto simp:child_def)+
−
  moreover have "(z, Th th') \<in> (child s')^+" by fact+
−
  ultimately show ?case by auto+
−
qed+
−
+
−
lemma eq_child_right:+
−
  shows "(n1, Th th') \<in> (child s')^+ \<Longrightarrow> (n1, Th th') \<in> (child s)^+"+
−
proof(induct rule:converse_trancl_induct)+
−
  case (base y)+
−
  with RAG_s show ?case by (auto simp:child_def)+
−
next+
−
  case (step y z)+
−
  have "(y, z) \<in> child s'" by fact+
−
  with RAG_s have "(y, z) \<in> child s" by (auto simp:child_def)+
−
  moreover have "(z, Th th') \<in> (child s)^+" by fact+
−
  ultimately show ?case by auto+
−
qed+
−
+
−
lemma eq_child:+
−
  assumes nd: "(Th th, Th th') \<notin> (child s)^+"+
−
  shows "((n1, Th th') \<in> (child s)^+) = ((n1, Th th') \<in> (child s')^+)"+
−
  by (insert eq_child_left[OF nd] eq_child_right, auto)+
−
+
−
lemma eq_cp:+
−
  fixes th' +
−
  assumes nd: "th \<notin> dependants s th'"+
−
  shows "cp s th' = cp s' th'"+
−
  apply (unfold cp_eq_cpreced cpreced_def)+
−
proof -+
−
  have nd': "(Th th, Th th') \<notin> (child s)^+"+
−
  proof+
−
    assume "(Th th, Th th') \<in> (child s)\<^sup>+"+
−
    with child_RAG_eq[OF vt_s]+
−
    have "(Th th, Th th') \<in> (RAG s)\<^sup>+" by simp+
−
    with nd show False +
−
      by (simp add:s_dependants_def eq_RAG)+
−
  qed+
−
  have eq_dp: "dependants (wq s) th' = dependants (wq s') th'"+
−
  proof(auto)+
−
    fix x assume " x \<in> dependants (wq s) th'"+
−
    thus "x \<in> dependants (wq s') th'"+
−
      apply (auto simp:cs_dependants_def eq_RAG)+
−
    proof -+
−
      assume "(Th x, Th th') \<in> (RAG s)\<^sup>+"+
−
      with  child_RAG_eq[OF vt_s] have "(Th x, Th th') \<in> (child s)\<^sup>+" by simp+
−
      with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s')^+" by simp+
−
      with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]+
−
      show "(Th x, Th th') \<in> (RAG s')\<^sup>+" by simp+
−
    qed+
−
  next+
−
    fix x assume "x \<in> dependants (wq s') th'"+
−
    thus "x \<in> dependants (wq s) th'"+
−
      apply (auto simp:cs_dependants_def eq_RAG)+
−
    proof -+
−
      assume "(Th x, Th th') \<in> (RAG s')\<^sup>+"+
−
      with child_RAG_eq[OF step_back_vt[OF vt_s[unfolded s_def]]] +
−
      have "(Th x, Th th') \<in> (child s')\<^sup>+" by simp+
−
      with eq_child[OF nd'] have "(Th x, Th th') \<in> (child s)^+" by simp+
−
      with  child_RAG_eq[OF vt_s]+
−
      show "(Th x, Th th') \<in> (RAG s)\<^sup>+" by simp+
−
    qed+
−
  qed+
−
  moreover {+
−
    fix th1 have "preced th1 s = preced th1 s'" by (simp add:s_def preced_def)+
−
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = +
−
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" +
−
    by (auto simp:image_def)+
−
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =+
−
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp+
−
qed+
−
+
−
lemma eq_up:+
−
  fixes th' th''+
−
  assumes dp1: "th \<in> dependants s th'"+
−
  and dp2: "th' \<in> dependants s th''"+
−
  and eq_cps: "cp s th' = cp s' th'"+
−
  shows "cp s th'' = cp s' th''"+
−
proof -+
−
  from dp2+
−
  have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)+
−
  from RAG_child[OF vt_s this[unfolded eq_RAG]]+
−
  have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .+
−
  moreover {+
−
    fix n th''+
−
    have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>+
−
                   (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"+
−
    proof(erule trancl_induct, auto)+
−
      fix y th''+
−
      assume y_ch: "(y, Th th'') \<in> child s"+
−
        and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"+
−
        and ch': "(Th th', y) \<in> (child s)\<^sup>+"+
−
      from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)+
−
      with ih have eq_cpy:"cp s thy = cp s' thy" by blast+
−
      from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)+
−
      moreover from child_RAG_p[OF ch'] and eq_y+
−
      have "(Th th', Th thy) \<in> (RAG s)^+" by simp+
−
      ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto+
−
      show "cp s th'' = cp s' th''"+
−
        apply (subst cp_rec[OF vt_s])+
−
      proof -+
−
        have "preced th'' s = preced th'' s'"+
−
          by (simp add:s_def preced_def)+
−
        moreover { +
−
          fix th1+
−
          assume th1_in: "th1 \<in> children s th''"+
−
          have "cp s th1 = cp s' th1"+
−
          proof(cases "th1 = thy")+
−
            case True+
−
            with eq_cpy show ?thesis by simp+
−
          next+
−
            case False+
−
            have neq_th1: "th1 \<noteq> th"+
−
            proof+
−
              assume eq_th1: "th1 = th"+
−
              with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp+
−
              from children_no_dep[OF vt_s _ _ this] and +
−
              th1_in y_ch eq_y show False by (auto simp:children_def)+
−
            qed+
−
            have "th \<notin> dependants s th1"+
−
            proof+
−
              assume h:"th \<in> dependants s th1"+
−
              from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)+
−
              from dependants_child_unique[OF vt_s _ _ h this]+
−
              th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)+
−
              with False show False by auto+
−
            qed+
−
            from eq_cp[OF this]+
−
            show ?thesis .+
−
          qed+
−
        }+
−
        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = +
−
          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)+
−
        moreover have "children s th'' = children s' th''"+
−
          apply (unfold children_def child_def s_def RAG_set_unchanged, simp)+
−
          apply (fold s_def, auto simp:RAG_s)+
−
          proof -+
−
            assume "(Cs cs, Th th'') \<in> RAG s'"+
−
            with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto+
−
            from dp1 have "(Th th, Th th') \<in> (RAG s)^+"+
−
              by (auto simp:s_dependants_def eq_RAG)+
−
            from converse_tranclE[OF this]+
−
            obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"+
−
              and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"+
−
              by (auto simp:s_RAG_def)+
−
            have eq_cs: "cs1 = cs" +
−
            proof -+
−
              from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp+
−
              from unique_RAG[OF vt_s this h1]+
−
              show ?thesis by simp+
−
            qed+
−
            have False+
−
            proof(rule converse_tranclE[OF h2])+
−
              assume "(Cs cs1, Th th') \<in> RAG s"+
−
              with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp+
−
              from unique_RAG[OF vt_s this cs_th']+
−
              have "th' = th''" by simp+
−
              with ch' y_ch have "(Th th'', Th th'') \<in> (child s)^+" by auto+
−
              with wf_trancl[OF wf_child[OF vt_s]] +
−
              show False by auto+
−
            next+
−
              fix y+
−
              assume "(Cs cs1, y) \<in> RAG s"+
−
                and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"+
−
              with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp+
−
              from unique_RAG[OF vt_s this cs_th']+
−
              have "y = Th th''" .+
−
              with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp+
−
              from RAG_child[OF vt_s this]+
−
              have "(Th th'', Th th') \<in> (child s)\<^sup>+" .+
−
              moreover from ch' y_ch have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto+
−
              ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto +
−
              with wf_trancl[OF wf_child[OF vt_s]] +
−
              show False by auto+
−
            qed+
−
            thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto+
−
          qed+
−
          ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"+
−
          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])+
−
      qed+
−
    next+
−
      fix th''+
−
      assume dp': "(Th th', Th th'') \<in> child s"+
−
      show "cp s th'' = cp s' th''"+
−
        apply (subst cp_rec[OF vt_s])+
−
      proof -+
−
        have "preced th'' s = preced th'' s'"+
−
          by (simp add:s_def preced_def)+
−
        moreover { +
−
          fix th1+
−
          assume th1_in: "th1 \<in> children s th''"+
−
          have "cp s th1 = cp s' th1"+
−
          proof(cases "th1 = th'")+
−
            case True+
−
            with eq_cps show ?thesis by simp+
−
          next+
−
            case False+
−
            have neq_th1: "th1 \<noteq> th"+
−
            proof+
−
              assume eq_th1: "th1 = th"+
−
              with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" +
−
                by (auto simp:s_dependants_def eq_RAG)+
−
              from children_no_dep[OF vt_s _ _ this]+
−
              th1_in dp'+
−
              show False by (auto simp:children_def)+
−
            qed+
−
            show ?thesis+
−
            proof(rule eq_cp)+
−
              show "th \<notin> dependants s th1"+
−
              proof+
−
                assume "th \<in> dependants s th1"+
−
                from dependants_child_unique[OF vt_s _ _ this dp1]+
−
                th1_in dp' have "th1 = th'"+
−
                  by (auto simp:children_def)+
−
                with False show False by auto+
−
              qed+
−
            qed+
−
          qed+
−
        }+
−
        ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = +
−
          {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)+
−
        moreover have "children s th'' = children s' th''"+
−
          apply (unfold children_def child_def s_def RAG_set_unchanged, simp)+
−
          apply (fold s_def, auto simp:RAG_s)+
−
          proof -+
−
            assume "(Cs cs, Th th'') \<in> RAG s'"+
−
            with RAG_s have cs_th': "(Cs cs, Th th'') \<in> RAG s" by auto+
−
            from dp1 have "(Th th, Th th') \<in> (RAG s)^+"+
−
              by (auto simp:s_dependants_def eq_RAG)+
−
            from converse_tranclE[OF this]+
−
            obtain cs1 where h1: "(Th th, Cs cs1) \<in> RAG s"+
−
              and h2: "(Cs cs1 , Th th') \<in> (RAG s)\<^sup>+"+
−
              by (auto simp:s_RAG_def)+
−
            have eq_cs: "cs1 = cs" +
−
            proof -+
−
              from RAG_s have "(Th th, Cs cs) \<in> RAG s" by simp+
−
              from unique_RAG[OF vt_s this h1]+
−
              show ?thesis by simp+
−
            qed+
−
            have False+
−
            proof(rule converse_tranclE[OF h2])+
−
              assume "(Cs cs1, Th th') \<in> RAG s"+
−
              with eq_cs have "(Cs cs, Th th') \<in> RAG s" by simp+
−
              from unique_RAG[OF vt_s this cs_th']+
−
              have "th' = th''" by simp+
−
              with dp' have "(Th th'', Th th'') \<in> (child s)^+" by auto+
−
              with wf_trancl[OF wf_child[OF vt_s]] +
−
              show False by auto+
−
            next+
−
              fix y+
−
              assume "(Cs cs1, y) \<in> RAG s"+
−
                and ytd: " (y, Th th') \<in> (RAG s)\<^sup>+"+
−
              with eq_cs have csy: "(Cs cs, y) \<in> RAG s" by simp+
−
              from unique_RAG[OF vt_s this cs_th']+
−
              have "y = Th th''" .+
−
              with ytd have "(Th th'', Th th') \<in> (RAG s)^+" by simp+
−
              from RAG_child[OF vt_s this]+
−
              have "(Th th'', Th th') \<in> (child s)\<^sup>+" .+
−
              moreover from dp' have ch'': "(Th th', Th th'') \<in> (child s)^+" by auto+
−
              ultimately have "(Th th'', Th th'') \<in> (child s)^+" by auto +
−
              with wf_trancl[OF wf_child[OF vt_s]] +
−
              show False by auto+
−
            qed+
−
            thus "\<exists>cs. (Th th, Cs cs) \<in> RAG s' \<and> (Cs cs, Th th'') \<in> RAG s'" by auto+
−
          qed+
−
        ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"+
−
          by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])+
−
      qed     +
−
    qed+
−
  }+
−
  ultimately show ?thesis by auto+
−
qed+
−
+
−
end+
−
+
−
locale step_create_cps =+
−
  fixes s' th prio s +
−
  defines s_def : "s \<equiv> (Create th prio#s')"+
−
  assumes vt_s: "vt s"+
−
+
−
context step_create_cps+
−
begin+
−
+
−
lemma eq_dep: "RAG s = RAG s'"+
−
  by (unfold s_def RAG_create_unchanged, auto)+
−
+
−
lemma eq_cp:+
−
  fixes th' +
−
  assumes neq_th: "th' \<noteq> th"+
−
  shows "cp s th' = cp s' th'"+
−
  apply (unfold cp_eq_cpreced cpreced_def)+
−
proof -+
−
  have nd: "th \<notin> dependants s th'"+
−
  proof+
−
    assume "th \<in> dependants s th'"+
−
    hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)+
−
    with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp+
−
    from converse_tranclE[OF this]+
−
    obtain y where "(Th th, y) \<in> RAG s'" by auto+
−
    with dm_RAG_threads[OF step_back_vt[OF vt_s[unfolded s_def]]]+
−
    have in_th: "th \<in> threads s'" by auto+
−
    from step_back_step[OF vt_s[unfolded s_def]]+
−
    show False+
−
    proof(cases)+
−
      assume "th \<notin> threads s'" +
−
      with in_th show ?thesis by simp+
−
    qed+
−
  qed+
−
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"+
−
    by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)+
−
  moreover {+
−
    fix th1 +
−
    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"+
−
    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto+
−
    hence "preced th1 s = preced th1 s'"+
−
    proof+
−
      assume "th1 = th'"+
−
      with neq_th+
−
      show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)+
−
    next+
−
      assume "th1 \<in> dependants (wq s') th'"+
−
      with nd and eq_dp have "th1 \<noteq> th"+
−
        by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)+
−
      thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)+
−
    qed+
−
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = +
−
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" +
−
    by (auto simp:image_def)+
−
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =+
−
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp+
−
qed+
−
+
−
lemma nil_dependants: "dependants s th = {}"+
−
proof -+
−
  from step_back_step[OF vt_s[unfolded s_def]]+
−
  show ?thesis+
−
  proof(cases)+
−
    assume "th \<notin> threads s'"+
−
    from not_thread_holdents[OF step_back_vt[OF vt_s[unfolded s_def]] this]+
−
    have hdn: " holdents s' th = {}" .+
−
    have "dependants s' th = {}"+
−
    proof -+
−
      { assume "dependants s' th \<noteq> {}"+
−
        then obtain th' where dp: "(Th th', Th th) \<in> (RAG s')^+"+
−
          by (auto simp:s_dependants_def eq_RAG)+
−
        from tranclE[OF this] obtain cs' where +
−
          "(Cs cs', Th th) \<in> RAG s'" by (auto simp:s_RAG_def)+
−
        with hdn+
−
        have False by (auto simp:holdents_test)+
−
      } thus ?thesis by auto+
−
    qed+
−
    thus ?thesis +
−
      by (unfold s_def s_dependants_def eq_RAG RAG_create_unchanged, simp)+
−
  qed+
−
qed+
−
+
−
lemma eq_cp_th: "cp s th = preced th s"+
−
  apply (unfold cp_eq_cpreced cpreced_def)+
−
  by (insert nil_dependants, unfold s_dependants_def cs_dependants_def, auto)+
−
+
−
end+
−
+
−
+
−
locale step_exit_cps =+
−
  fixes s' th prio s +
−
  defines s_def : "s \<equiv> Exit th # s'"+
−
  assumes vt_s: "vt s"+
−
+
−
context step_exit_cps+
−
begin+
−
+
−
lemma eq_dep: "RAG s = RAG s'"+
−
  by (unfold s_def RAG_exit_unchanged, auto)+
−
+
−
lemma eq_cp:+
−
  fixes th' +
−
  assumes neq_th: "th' \<noteq> th"+
−
  shows "cp s th' = cp s' th'"+
−
  apply (unfold cp_eq_cpreced cpreced_def)+
−
proof -+
−
  have nd: "th \<notin> dependants s th'"+
−
  proof+
−
    assume "th \<in> dependants s th'"+
−
    hence "(Th th, Th th') \<in> (RAG s)^+" by (simp add:s_dependants_def eq_RAG)+
−
    with eq_dep have "(Th th, Th th') \<in> (RAG s')^+" by simp+
−
    from converse_tranclE[OF this]+
−
    obtain cs' where bk: "(Th th, Cs cs') \<in> RAG s'"+
−
      by (auto simp:s_RAG_def)+
−
    from step_back_step[OF vt_s[unfolded s_def]]+
−
    show False+
−
    proof(cases)+
−
      assume "th \<in> runing s'"+
−
      with bk show ?thesis+
−
        apply (unfold runing_def readys_def s_waiting_def s_RAG_def)+
−
        by (auto simp:cs_waiting_def wq_def)+
−
    qed+
−
  qed+
−
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"+
−
    by (unfold cs_dependants_def, auto simp:eq_dep eq_RAG)+
−
  moreover {+
−
    fix th1 +
−
    assume "th1 \<in> {th'} \<union> dependants (wq s') th'"+
−
    hence "th1 = th' \<or> th1 \<in> dependants (wq s') th'" by auto+
−
    hence "preced th1 s = preced th1 s'"+
−
    proof+
−
      assume "th1 = th'"+
−
      with neq_th+
−
      show "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)+
−
    next+
−
      assume "th1 \<in> dependants (wq s') th'"+
−
      with nd and eq_dp have "th1 \<noteq> th"+
−
        by (auto simp:eq_RAG cs_dependants_def s_dependants_def eq_dep)+
−
      thus "preced th1 s = preced th1 s'" by (auto simp:s_def preced_def)+
−
    qed+
−
  } ultimately have "((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) = +
−
                     ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" +
−
    by (auto simp:image_def)+
−
  thus "Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependants (wq s) th')) =+
−
        Max ((\<lambda>th. preced th s') ` ({th'} \<union> dependants (wq s') th'))" by simp+
−
qed+
−
+
−
end+
−
end+
−
+
−