+
−
theory CpsG+
−
imports PrioG +
−
begin+
−
+
−
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:depend_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 depend_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 depend_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_depend_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_depend_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:depend_set_unchanged)+
−
    qed+
−
    next+
−
      case vt_nil+
−
      show ?case+
−
      by (auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def)+
−
  qed+
−
qed+
−
+
−
+
−
+
−
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+
−
+
−
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_depend:+
−
  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)" .+
−
qed+
−
+
−
lemma Max_Union:+
−
  assumes fc: "finite C"+
−
  and ne: "C \<noteq> {}"+
−
  and fa: "\<And> A. A \<in> C \<Longrightarrow> finite A \<and> A \<noteq> {}"+
−
  shows "Max (\<Union> C) = Max (Max ` C)"+
−
proof -+
−
  from fc ne fa show ?thesis+
−
  proof(induct)+
−
    case (insert x F)+
−
    assume ih: "\<lbrakk>F \<noteq> {}; \<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}\<rbrakk> \<Longrightarrow> Max (\<Union>F) = Max (Max ` F)"+
−
    and h: "\<And> A. A \<in> insert x F \<Longrightarrow> finite A \<and> A \<noteq> {}"+
−
    show ?case (is "?L = ?R")+
−
    proof(cases "F = {}")+
−
      case False+
−
      from Union_insert have "?L = Max (x \<union> (\<Union> F))" by simp+
−
      also have "\<dots> = max (Max x) (Max(\<Union> F))"+
−
      proof(rule Max_Un)+
−
        from h[of x] show "finite x" by auto+
−
      next+
−
        from h[of x] show "x \<noteq> {}" by auto+
−
      next+
−
        show "finite (\<Union>F)"+
−
        proof(rule finite_Union)+
−
          show "finite F" by fact+
−
        next+
−
          from h show "\<And>M. M \<in> F \<Longrightarrow> finite M" by auto+
−
        qed+
−
      next+
−
        from False and h show "\<Union>F \<noteq> {}" by auto+
−
      qed+
−
      also have "\<dots> = ?R"+
−
      proof -+
−
        have "?R = Max (Max ` ({x} \<union> F))" by simp+
−
        also have "\<dots> = Max ({Max x} \<union> (Max ` F))" by simp+
−
        also have "\<dots> = max (Max x) (Max (\<Union>F))"+
−
        proof -+
−
          have "Max ({Max x} \<union> Max ` F) = max (Max {Max x}) (Max (Max ` F))"+
−
          proof(rule Max_Un)+
−
            show "finite {Max x}" by simp+
−
          next+
−
            show "{Max x} \<noteq> {}" by simp+
−
          next+
−
            from insert show "finite (Max ` F)" by auto+
−
          next+
−
            from False show "Max ` F \<noteq> {}" by auto+
−
          qed+
−
          moreover have "Max {Max x} = Max x" by simp+
−
          moreover have "Max (\<Union>F) = Max (Max ` F)"+
−
          proof(rule ih)+
−
            show "F \<noteq> {}" by fact+
−
          next+
−
            from h show "\<And>A. A \<in> F \<Longrightarrow> finite A \<and> A \<noteq> {}"+
−
              by auto+
−
          qed+
−
          ultimately show ?thesis by auto+
−
        qed+
−
        finally show ?thesis by simp+
−
      qed+
−
      finally show ?thesis by simp+
−
    next+
−
      case True+
−
      thus ?thesis by auto+
−
    qed+
−
  next+
−
    case empty+
−
    assume "{} \<noteq> {}" show ?case by auto+
−
  qed+
−
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> depend s \<and> (Cs cs, Th th) \<in> depend 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> depend s \<and> (Cs cs, Th th) \<in> depend s}"+
−
unfolding child_def children_def by simp+
−
+
−
lemma children_dependants: "children s th \<subseteq> dependants (wq s) th"+
−
  by (unfold children_def child_def cs_dependants_def, auto simp:eq_depend)+
−
+
−
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> depend s"+
−
    and h2: "(Cs cs, Th th1) \<in> depend s"+
−
    and h3: "(Th th, Cs csa) \<in> depend s"+
−
    and h4: "(Cs csa, Th th2) \<in> depend s"+
−
  from unique_depend[OF vt h1 h3] have "cs = csa" by simp+
−
  with h4 have "(Cs cs, Th th2) \<in> depend s" by simp+
−
  from unique_depend[OF vt h2 this]+
−
  show "th1 = th2" by simp+
−
qed +
−
+
−
lemma depend_children:+
−
  assumes h: "(Th th1, Th th2) \<in> (depend s)^+"+
−
  shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)^+)"+
−
proof -+
−
  from h show ?thesis+
−
  proof(induct rule: tranclE)+
−
    fix c th2+
−
    assume h1: "(Th th1, c) \<in> (depend s)\<^sup>+"+
−
    and h2: "(c, Th th2) \<in> depend s"+
−
    from h2 obtain cs where eq_c: "c = Cs cs"+
−
      by (case_tac c, auto simp:s_depend_def)+
−
    show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"+
−
    proof(rule tranclE[OF h1])+
−
      fix ca+
−
      assume h3: "(Th th1, ca) \<in> (depend s)\<^sup>+"+
−
        and h4: "(ca, c) \<in> depend s"+
−
      show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (depend s)\<^sup>+)"+
−
      proof -+
−
        from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"+
−
          by (case_tac ca, auto simp:s_depend_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> (depend s)\<^sup>+" by simp+
−
        ultimately show ?thesis by auto+
−
      qed+
−
    next+
−
      assume "(Th th1, c) \<in> depend 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> depend s"+
−
    thus ?thesis+
−
      by (auto simp:s_depend_def)+
−
  qed+
−
qed+
−
+
−
lemma sub_child: "child s \<subseteq> (depend 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_depend[OF vt]])+
−
apply(rule sub_child)+
−
done+
−
+
−
lemma depend_child_pre:+
−
  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)^+)" .+
−
  show ?thesis+
−
  proof(rule wf_induct[OF wf, of ?P], clarsimp)+
−
    fix th'+
−
    assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (depend s)\<^sup>+ \<longrightarrow>+
−
               (Th th, y) \<in> (depend s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"+
−
    and h: "(Th th, Th th') \<in> (depend s)\<^sup>+"+
−
    show "(Th th, Th th') \<in> (child s)\<^sup>+"+
−
    proof -+
−
      from depend_children[OF h]+
−
      have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (depend 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> (depend s)\<^sup>+"+
−
        then obtain th3 where th3_in: "th3 \<in> children s th'" +
−
          and th_dp: "(Th th, Th th3) \<in> (depend s)\<^sup>+" by auto+
−
        from th3_in have "(Th th3, Th th') \<in> (depend 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 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)^+"+
−
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> (depend s)^+" by auto+
−
    moreover have "(n1, y) \<in> (depend s)^+" by fact+
−
    ultimately show ?case by auto+
−
  qed+
−
qed+
−
+
−
lemma child_depend_eq: +
−
  assumes vt: "vt s"+
−
  shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (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 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 -+
−
  from depend_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+
−
+
−
lemma unique_depend_p:+
−
  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])+
−
  from unique_depend[OF vt]+
−
  show "\<And>a b c. \<lbrakk>(a, b) \<in> depend s; (a, c) \<in> depend s\<rbrakk> \<Longrightarrow> b = c" by auto+
−
qed+
−
+
−
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> (depend s)^+" +
−
      by (simp add:s_dependants_def eq_depend)+
−
    from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+" +
−
      by (simp add:s_dependants_def eq_depend)+
−
    from unique_depend_p[OF vt dp1 dp2] and neq+
−
    have "(Th th1, Th th2) \<in> (depend s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (depend s)\<^sup>+" by auto+
−
    hence False+
−
    proof+
−
      assume "(Th th1, Th th2) \<in> (depend s)\<^sup>+ "+
−
      from children_no_dep[OF vt ch1 ch2 this] show ?thesis .+
−
    next+
−
      assume " (Th th2, Th th1) \<in> (depend s)\<^sup>+"+
−
      from children_no_dep[OF vt ch2 ch1 this] show ?thesis .+
−
    qed+
−
  } thus ?thesis by auto+
−
qed+
−
+
−
lemma depend_plus_elim:+
−
  assumes "vt s"+
−
  fixes x+
−
  assumes "(Th x, Th th) \<in> (depend (wq s))\<^sup>+"+
−
  shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (depend (wq s))\<^sup>+"+
−
  using assms(2)[unfolded eq_depend, folded child_depend_eq[OF `vt s`]]+
−
  apply (unfold children_def)+
−
  by (metis assms(2) children_def depend_children eq_depend)+
−
+
−
lemma dependants_expand_pre: +
−
  assumes "vt s"+
−
  shows "dependants (wq s) th = (\<Union> th' \<in> children s th. {th'} \<union> dependants (wq s) th')"+
−
  apply (unfold cs_dependants_def)+
−
  apply (auto elim!:depend_plus_elim[OF assms])+
−
  apply (metis children_def eq_depend mem_Collect_eq set_mp sub_child)+
−
  apply (unfold children_def, auto)+
−
  apply (unfold eq_depend, fold  child_depend_eq[OF `vt s`])+
−
  by (metis trancl.simps)+
−
+
−
lemma dependants_expand:+
−
  assumes "vt s"+
−
  shows "dependants (wq s) th = (\<Union> ((\<lambda> th. {th} \<union> dependants (wq s) th) ` (children s th)))"+
−
  apply (subst dependants_expand_pre[OF assms])+
−
  by simp+
−
+
−
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)+
−
+
−
lemma Max_insert:+
−
  assumes "finite B"+
−
  and  "B \<noteq> {}"+
−
  shows "Max ({x} \<union> B) = max x (Max B)"+
−
  by (metis Max_insert assms insert_is_Un)+
−
+
−
lemma dependands_expand2:+
−
  assumes "vt s"+
−
  shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"+
−
  by (subst dependants_expand[OF assms]) (auto)+
−
+
−
abbreviation+
−
  "preceds s Ths \<equiv> {preced th s| th. th \<in> Ths}"+
−
+
−
lemma image_compr:+
−
  "f ` A = {f x | x. x \<in> A}"+
−
by auto+
−
+
−
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+
−
+
−
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_compr[symmetric])+
−
  +
−
    have not_emptyness_facts[simp]: +
−
      "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"+
−
      using False dependands_expand2[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 dependands_expand2[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+
−
+
−
definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"+
−
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 s"+
−
+
−
context step_set_cps +
−
begin+
−
+
−
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+
−
+
−
lemma eq_dep: "depend s = depend s'"+
−
  by (unfold s_def depend_set_unchanged, auto)+
−
+
−
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'"+
−
  apply (unfold cp_eq_cpreced cpreced_def)+
−
proof -+
−
  have eq_dp: "\<And> th. dependants (wq s) th = dependants (wq s') th"+
−
    by (unfold cs_dependants_def, auto simp:eq_dep eq_depend)+
−
  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 eq_preced[OF neq_th]+
−
      show "preced th1 s = preced th1 s'" by simp+
−
    next+
−
      assume "th1 \<in> dependants (wq s') th'"+
−
      with nd and eq_dp have "th1 \<noteq> th"+
−
        by (auto simp:eq_depend cs_dependants_def s_dependants_def eq_dep)+
−
      from eq_preced[OF this] show "preced th1 s = preced th1 s'" by simp+
−
    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 no_dependants:+
−
  assumes "th' \<noteq> th"+
−
  shows "th \<notin> dependants s th'"+
−
proof+
−
  assume h: "th \<in> dependants s th'"+
−
  from step_back_step [OF vt_s[unfolded s_def]]+
−
  have "step s' (Set th prio)" .+
−
  hence "th \<in> runing s'" by (cases, simp)+
−
  hence rd_th: "th \<in> readys s'" +
−
    by (simp add:readys_def runing_def)+
−
  from h have "(Th th, Th th') \<in> (depend s')\<^sup>+"+
−
    by (unfold s_dependants_def, unfold eq_depend, unfold eq_dep, auto)+
−
  from tranclD[OF this]+
−
  obtain z where "(Th th, z) \<in> depend s'" by auto+
−
  with rd_th show "False"+
−
    apply (case_tac z, auto simp:readys_def s_waiting_def s_depend_def s_waiting_def cs_waiting_def)+
−
    by (fold wq_def, blast)+
−
qed+
−
+
−
(* Result improved *)+
−
lemma eq_cp:+
−
 fixes th' +
−
  assumes neq_th: "th' \<noteq> th"+
−
  shows "cp s th' = cp s' th'"+
−
proof(rule eq_cp_pre [OF neq_th])+
−
  from no_dependants[OF neq_th] +
−
  show "th \<notin> dependants s th'" .+
−
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> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)+
−
  from depend_child[OF vt_s this[unfolded eq_depend]]+
−
  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> (depend s)^+" by (auto simp:s_dependants_def eq_depend)+
−
      moreover from child_depend_p[OF ch'] and eq_y+
−
      have "(Th th', Th thy) \<in> (depend s)^+" by simp+
−
      ultimately have dp_thy: "(Th th, Th thy) \<in> (depend 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'"+
−
        proof(rule eq_preced)+
−
          show "th'' \<noteq> th"+
−
          proof+
−
            assume "th'' = th"+
−
            with dp_thy y_ch[unfolded eq_y] +
−
            have "(Th th, Th th) \<in> (depend s)^+"+
−
              by (auto simp:child_def)+
−
            with wf_trancl[OF wf_depend[OF vt_s]] +
−
            show False by auto+
−
          qed+
−
        qed+
−
        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> (depend 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_depend)+
−
              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_pre[OF neq_th1 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''"+
−
          by (unfold children_def child_def s_def depend_set_unchanged, simp)+
−
        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'"+
−
        proof(rule eq_preced)+
−
          show "th'' \<noteq> th"+
−
          proof+
−
            assume "th'' = th"+
−
            with dp1 dp'+
−
            have "(Th th, Th th) \<in> (depend s)^+"+
−
              by (auto simp:child_def s_dependants_def eq_depend)+
−
            with wf_trancl[OF wf_depend[OF vt_s]] +
−
            show False by auto+
−
          qed+
−
        qed+
−
        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> (depend s)^+" +
−
                by (auto simp:s_dependants_def eq_depend)+
−
              from children_no_dep[OF vt_s _ _ this]+
−
              th1_in dp'+
−
              show False by (auto simp:children_def)+
−
            qed+
−
            thus ?thesis+
−
            proof(rule eq_cp_pre)+
−
              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''"+
−
          by (unfold children_def child_def s_def depend_set_unchanged, simp)+
−
        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+
−
+
−
lemma eq_up_self:+
−
  fixes th' th''+
−
  assumes dp: "th \<in> dependants s th''"+
−
  and eq_cps: "cp s th = cp s' th"+
−
  shows "cp s th'' = cp s' th''"+
−
proof -+
−
  from dp+
−
  have "(Th th, Th th'') \<in> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)+
−
  from depend_child[OF vt_s this[unfolded eq_depend]]+
−
  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 child_depend_p[OF ch'] and eq_y+
−
      have dp_thy: "(Th th, Th thy) \<in> (depend s)^+" by simp+
−
      show "cp s th'' = cp s' th''"+
−
        apply (subst cp_rec[OF vt_s])+
−
      proof -+
−
        have "preced th'' s = preced th'' s'"+
−
        proof(rule eq_preced)+
−
          show "th'' \<noteq> th"+
−
          proof+
−
            assume "th'' = th"+
−
            with dp_thy y_ch[unfolded eq_y] +
−
            have "(Th th, Th th) \<in> (depend s)^+"+
−
              by (auto simp:child_def)+
−
            with wf_trancl[OF wf_depend[OF vt_s]] +
−
            show False by auto+
−
          qed+
−
        qed+
−
        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> (depend 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_depend)+
−
              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_pre[OF neq_th1 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''"+
−
          by (unfold children_def child_def s_def depend_set_unchanged, simp)+
−
        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'"+
−
        proof(rule eq_preced)+
−
          show "th'' \<noteq> th"+
−
          proof+
−
            assume "th'' = th"+
−
            with dp dp'+
−
            have "(Th th, Th th) \<in> (depend s)^+"+
−
              by (auto simp:child_def s_dependants_def eq_depend)+
−
            with wf_trancl[OF wf_depend[OF vt_s]] +
−
            show False by auto+
−
          qed+
−
        qed+
−
        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+
−
            assume neq_th1: "th1 \<noteq> th"+
−
            thus ?thesis+
−
            proof(rule eq_cp_pre)+
−
              show "th \<notin> dependants s th1"+
−
              proof+
−
                assume "th \<in> dependants s th1"+
−
                hence "(Th th, Th th1) \<in> (depend s)^+" by (auto simp:s_dependants_def eq_depend)+
−
                from children_no_dep[OF vt_s _ _ this]+
−
                and th1_in dp' show False+
−
                  by (auto simp:children_def)+
−
              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''"+
−
          by (unfold children_def child_def s_def depend_set_unchanged, simp)+
−
        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+
−
+
−
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+
−
+
−
+
−
+
−
+
−
locale step_v_cps =+
−
  fixes s' th cs s +
−
  defines s_def : "s \<equiv> (V th cs#s')"+
−
  assumes vt_s: "vt s"+
−
+
−
locale step_v_cps_nt = step_v_cps ++
−
  fixes th'+
−
  assumes nt: "next_th s' th cs th'"+
−
+
−
context step_v_cps_nt+
−
begin+
−
+
−
lemma depend_s:+
−
  "depend s = (depend s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>+
−
                                         {(Cs cs, Th th')}"+
−
proof -+
−
  from step_depend_v[OF vt_s[unfolded s_def], folded s_def]+
−
    and nt show ?thesis  by (auto intro:next_th_unique)+
−
qed+
−
+
−
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)+
−
  fix x+
−
  assume "x \<in> dependants (wq s) th''"+
−
  hence dp: "(Th x, Th th'') \<in> (depend s)^+"+
−
    by (auto simp:cs_dependants_def eq_depend)+
−
  { fix n+
−
    have "(n, Th th'') \<in> (depend s)^+ \<Longrightarrow>  (n, Th th'') \<in> (depend s')^+"+
−
    proof(induct rule:converse_trancl_induct)+
−
      fix y +
−
      assume "(y, Th th'') \<in> depend s"+
−
      with depend_s neq1 neq2+
−
      have "(y, Th th'') \<in> depend s'" by auto+
−
      thus "(y, Th th'') \<in> (depend s')\<^sup>+" by auto+
−
    next+
−
      fix y z +
−
      assume yz: "(y, z) \<in> depend s"+
−
        and ztp: "(z, Th th'') \<in> (depend s)\<^sup>+"+
−
        and ztp': "(z, Th th'') \<in> (depend 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> depend s" by simp+
−
          from depend_s+
−
          have cst': "(Cs cs, Th th') \<in> depend s" by simp+
−
          from unique_depend[OF vt_s this dp_yz] +
−
          have eq_z: "z = Th th'" by simp+
−
          with ztp have "(Th th', Th th'') \<in> (depend s)^+" by simp+
−
          from converse_tranclE[OF this]+
−
          obtain cs' where dp'': "(Th th', Cs cs') \<in> depend s"+
−
            by (auto simp:s_depend_def)+
−
          with depend_s have dp': "(Th th', Cs cs') \<in> depend s'" by auto+
−
          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 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]]+
−
          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> depend s" by simp+
−
          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 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+
−
      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+
−
    qed    +
−
  }+
−
  from this[OF dp]+
−
  show "x \<in> dependants (wq s') th''" +
−
    by (auto simp:cs_dependants_def eq_depend)+
−
next+
−
  fix x+
−
  assume "x \<in> dependants (wq s') th''"+
−
  hence dp: "(Th x, Th th'') \<in> (depend s')^+"+
−
    by (auto simp:cs_dependants_def eq_depend)+
−
  { fix n+
−
    have "(n, Th th'') \<in> (depend s')^+ \<Longrightarrow>  (n, Th th'') \<in> (depend s)^+"+
−
    proof(induct rule:converse_trancl_induct)+
−
      fix y +
−
      assume "(y, Th th'') \<in> depend s'"+
−
      with depend_s neq1 neq2+
−
      have "(y, Th th'') \<in> depend s" by auto+
−
      thus "(y, Th th'') \<in> (depend s)\<^sup>+" by auto+
−
    next+
−
      fix y z +
−
      assume yz: "(y, z) \<in> depend s'"+
−
        and ztp: "(z, Th th'') \<in> (depend s')\<^sup>+"+
−
        and ztp': "(z, Th th'') \<in> (depend 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> 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: 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 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 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 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+
−
          qed+
−
          with converse_tranclE[OF cs_i]+
−
          obtain u where cu: "(Cs cs, u) \<in> depend s'"  +
−
            and u_t: "(u, Th th'') \<in> (depend s')\<^sup>+" by auto+
−
          have "u = Th th"+
−
          proof -+
−
            from unique_depend[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> (depend s')\<^sup>+" 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 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+
−
    qed    +
−
  }+
−
  from this[OF dp]+
−
  show "x \<in> dependants (wq s) th''"+
−
    by (auto simp:cs_dependants_def eq_depend)+
−
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> depend s'"+
−
proof+
−
  assume "(Th th1, Cs cs) \<in> depend s'"+
−
  thus "False"+
−
    apply (auto simp:s_depend_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 depend_s: "depend s = depend s' - {(Cs cs, Th th)}"+
−
proof -+
−
  from nnt and  step_depend_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> depend s'"+
−
      and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp+
−
      with nw_cs eq_cs show False by auto+
−
    qed+
−
    with h1 h2 depend_s have +
−
      h1': "(Th th1, Cs cs1) \<in> depend s" and+
−
      h2': "(Cs cs1, Th th2) \<in> depend 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> depend s'"+
−
      and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp+
−
      with nw_cs eq_cs show False by auto+
−
    qed+
−
    with h1 h2 depend_s have +
−
      h1': "(Th th1, Cs cs1) \<in> depend s" and+
−
      h2': "(Cs cs1, Th th2) \<in> depend 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 depend_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 depend_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_depend)+
−
  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_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]+
−
    show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend 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 depend_s: "depend s = depend s' \<union> {(Cs cs, Th th)}"+
−
proof -+
−
  from ee and  step_depend_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> depend s'"+
−
      and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp+
−
      with ee show False+
−
        by (auto simp:s_depend_def cs_waiting_def)+
−
    qed+
−
    with h1 h2 depend_s have +
−
      h1': "(Th th1, Cs cs1) \<in> depend s" and+
−
      h2': "(Cs cs1, Th th2) \<in> depend 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> depend s'"+
−
      and h2: "(Cs cs1, Th th2) \<in> depend 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> depend s'" by simp+
−
      with ee show False +
−
        by (auto simp:s_depend_def cs_waiting_def)+
−
    qed+
−
    with h1 h2 depend_s have +
−
      h1': "(Th th1, Cs cs1) \<in> depend s" and+
−
      h2': "(Cs cs1, Th th2) \<in> depend 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 depend_s+
−
    have "(n1, y) \<in> child s'"+
−
      apply (auto simp:child_def)+
−
      proof -+
−
        fix th'+
−
        assume "(Th th', Cs cs) \<in> depend s'"+
−
        with ee have "False"+
−
          by (auto simp:s_depend_def cs_waiting_def)+
−
        thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend s'" by auto +
−
      qed+
−
    thus ?case by auto+
−
  next+
−
    case (step y z)+
−
    have "(y, z) \<in> child s" by fact+
−
    with depend_s have "(y, z) \<in> child s'"+
−
      apply (auto simp:child_def)+
−
      proof -+
−
        fix th'+
−
        assume "(Th th', Cs cs) \<in> depend s'"+
−
        with ee have "False"+
−
          by (auto simp:s_depend_def cs_waiting_def)+
−
        thus "\<exists>cs. (Th th', Cs cs) \<in> depend s' \<and> (Cs cs, Th th) \<in> depend 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_depend)+
−
  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_depend_eq[OF vt_s] child_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]+
−
    show "\<And>th. {th'. (Th th', Th th) \<in> (depend s)\<^sup>+} = {th'. (Th th', Th th) \<in> (depend 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 depend_s: "depend s = depend s' \<union> {(Th th, Cs cs)}"+
−
proof -+
−
  from step_depend_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> depend s"+
−
    and h2: "(Cs cs1, Th th') \<in> depend 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 depend_s +
−
  have h1': "(Th th1, Cs cs1) \<in> depend s'" and +
−
       h2': "(Cs cs1, Th th') \<in> depend 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> depend s"+
−
    and h2: "(Cs cs1, Th th2) \<in> depend 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 depend_s have h1': "(Th th1, Cs cs1) \<in> depend s'"+
−
                       and h2': "(Cs cs1, Th th2) \<in> depend 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 depend_s show ?case by (auto simp:child_def)+
−
next+
−
  case (step y z)+
−
  have "(y, z) \<in> child s'" by fact+
−
  with depend_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_depend_eq[OF vt_s]+
−
    have "(Th th, Th th') \<in> (depend s)\<^sup>+" by simp+
−
    with nd show False +
−
      by (simp add:s_dependants_def eq_depend)+
−
  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_depend)+
−
    proof -+
−
      assume "(Th x, Th th') \<in> (depend s)\<^sup>+"+
−
      with  child_depend_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_depend_eq[OF step_back_vt[OF vt_s[unfolded s_def]]]+
−
      show "(Th x, Th th') \<in> (depend 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_depend)+
−
    proof -+
−
      assume "(Th x, Th th') \<in> (depend s')\<^sup>+"+
−
      with child_depend_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_depend_eq[OF vt_s]+
−
      show "(Th x, Th th') \<in> (depend 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> (depend (wq s))\<^sup>+" by (simp add:s_dependants_def)+
−
  from depend_child[OF vt_s this[unfolded eq_depend]]+
−
  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> (depend s)^+" by (auto simp:s_dependants_def eq_depend)+
−
      moreover from child_depend_p[OF ch'] and eq_y+
−
      have "(Th th', Th thy) \<in> (depend s)^+" by simp+
−
      ultimately have dp_thy: "(Th th, Th thy) \<in> (depend 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> (depend 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_depend)+
−
              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 depend_set_unchanged, simp)+
−
          apply (fold s_def, auto simp:depend_s)+
−
          proof -+
−
            assume "(Cs cs, Th th'') \<in> depend s'"+
−
            with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto+
−
            from dp1 have "(Th th, Th th') \<in> (depend s)^+"+
−
              by (auto simp:s_dependants_def eq_depend)+
−
            from converse_tranclE[OF this]+
−
            obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"+
−
              and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"+
−
              by (auto simp:s_depend_def)+
−
            have eq_cs: "cs1 = cs" +
−
            proof -+
−
              from depend_s have "(Th th, Cs cs) \<in> depend s" by simp+
−
              from unique_depend[OF vt_s this h1]+
−
              show ?thesis by simp+
−
            qed+
−
            have False+
−
            proof(rule converse_tranclE[OF h2])+
−
              assume "(Cs cs1, Th th') \<in> depend s"+
−
              with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp+
−
              from unique_depend[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> depend s"+
−
                and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"+
−
              with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp+
−
              from unique_depend[OF vt_s this cs_th']+
−
              have "y = Th th''" .+
−
              with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp+
−
              from depend_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> depend s' \<and> (Cs cs, Th th'') \<in> depend 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> (depend s)^+" +
−
                by (auto simp:s_dependants_def eq_depend)+
−
              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 depend_set_unchanged, simp)+
−
          apply (fold s_def, auto simp:depend_s)+
−
          proof -+
−
            assume "(Cs cs, Th th'') \<in> depend s'"+
−
            with depend_s have cs_th': "(Cs cs, Th th'') \<in> depend s" by auto+
−
            from dp1 have "(Th th, Th th') \<in> (depend s)^+"+
−
              by (auto simp:s_dependants_def eq_depend)+
−
            from converse_tranclE[OF this]+
−
            obtain cs1 where h1: "(Th th, Cs cs1) \<in> depend s"+
−
              and h2: "(Cs cs1 , Th th') \<in> (depend s)\<^sup>+"+
−
              by (auto simp:s_depend_def)+
−
            have eq_cs: "cs1 = cs" +
−
            proof -+
−
              from depend_s have "(Th th, Cs cs) \<in> depend s" by simp+
−
              from unique_depend[OF vt_s this h1]+
−
              show ?thesis by simp+
−
            qed+
−
            have False+
−
            proof(rule converse_tranclE[OF h2])+
−
              assume "(Cs cs1, Th th') \<in> depend s"+
−
              with eq_cs have "(Cs cs, Th th') \<in> depend s" by simp+
−
              from unique_depend[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> depend s"+
−
                and ytd: " (y, Th th') \<in> (depend s)\<^sup>+"+
−
              with eq_cs have csy: "(Cs cs, y) \<in> depend s" by simp+
−
              from unique_depend[OF vt_s this cs_th']+
−
              have "y = Th th''" .+
−
              with ytd have "(Th th'', Th th') \<in> (depend s)^+" by simp+
−
              from depend_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> depend s' \<and> (Cs cs, Th th'') \<in> depend 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: "depend s = depend s'"+
−
  by (unfold s_def depend_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> (depend s)^+" by (simp add:s_dependants_def eq_depend)+
−
    with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp+
−
    from converse_tranclE[OF this]+
−
    obtain y where "(Th th, y) \<in> depend s'" by auto+
−
    with dm_depend_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_depend)+
−
  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_depend 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> (depend s')^+"+
−
          by (auto simp:s_dependants_def eq_depend)+
−
        from tranclE[OF this] obtain cs' where +
−
          "(Cs cs', Th th) \<in> depend s'" by (auto simp:s_depend_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_depend depend_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: "depend s = depend s'"+
−
  by (unfold s_def depend_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> (depend s)^+" by (simp add:s_dependants_def eq_depend)+
−
    with eq_dep have "(Th th, Th th') \<in> (depend s')^+" by simp+
−
    from converse_tranclE[OF this]+
−
    obtain cs' where bk: "(Th th, Cs cs') \<in> depend s'"+
−
      by (auto simp:s_depend_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_depend_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_depend)+
−
  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_depend 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+
−
+
−