theory CpsG

imports PrioG 

begin

lemma not_thread_holdents:

  fixes th s

  assumes vt: "vt step s"

  and not_in: "th \<notin> threads s" 

  shows "holdents s th = {}"

proof -

  from vt not_in show ?thesis

  proof(induct arbitrary:th)

    case (vt_cons s e th)

    assume vt: "vt step s"

      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_def)

        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_def 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_def 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 prems have vtp: "vt step (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_def 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 prems have vtv: "vt step (V thread cs#s)" by auto

      from hold obtain rest 

        where eq_wq: "wq s cs = thread # rest"

        by (case_tac "wq s cs", auto simp:s_holding_def)

      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_def 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_def)

        by (simp add:depend_set_unchanged)

    qed

    next

      case vt_nil

      show ?case

      by (auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def)

  qed

qed

lemma next_th_neq: 

  assumes vt: "vt step 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"

proof -

  from assms show ?thesis

    by (unfold next_th_def, auto)

qed

lemma pp_sub: "(r^+)^+ \<subseteq> r^+"

  by auto

lemma wf_depend:

  assumes vt: "vt step 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 =

            {(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 = {th'. (Th th', Th th) \<in> child s}"

lemma children_dependents: "children s th \<subseteq> dependents (wq s) th"

  by (unfold children_def child_def cs_dependents_def, auto simp:eq_depend)

lemma child_unique:

  assumes vt: "vt step s"

  and ch1: "(Th th, Th th1) \<in> child s"

  and ch2: "(Th th, Th th2) \<in> child s"

  shows "th1 = th2"

proof -

  from ch1 ch2 show ?thesis

  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 

qed

lemma cp_eq_cpreced_f: "cp s = cpreced (wq s) s"

proof -

  from fun_eq_iff 

  have h:"\<And>f g. (\<forall> x. f x = g x) \<Longrightarrow> f = g" by auto

  show ?thesis

  proof(rule h)

    from cp_eq_cpreced show "\<forall>x. cp s x = cpreced (wq s) s x" by auto

  qed

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 step s"

  shows "wf (child s)"

proof(rule wf_subset)

  from wf_trancl[OF wf_depend[OF vt]]

  show "wf ((depend s)\<^sup>+)" .

next

  from sub_child show "child s \<subseteq> (depend s)\<^sup>+" .

qed

lemma depend_child_pre:

  assumes vt: "vt step s"

  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 step 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 step s"

  shows 

  "((Th th1, Th th2) \<in> (child s)^+) = 

   ((Th th1, Th th2) \<in> (depend s)^+)"

  by (auto intro: depend_child[OF vt] child_depend_p)

lemma children_no_dep:

  fixes s th th1 th2 th3

  assumes vt: "vt step s"

  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)

    thm tranclD

    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 step 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 dependents_child_unique:

  fixes s th th1 th2 th3

  assumes vt: "vt step s"

  and ch1: "(Th th1, Th th) \<in> child s"

  and ch2: "(Th th2, Th th) \<in> child s"

  and dp1: "th3 \<in> dependents s th1"

  and dp2: "th3 \<in> dependents s th2"

shows "th1 = th2"

proof -

  { assume neq: "th1 \<noteq> th2"

    from dp1 have dp1: "(Th th3, Th th1) \<in> (depend s)^+" 

      by (simp add:s_dependents_def eq_depend)

    from dp2 have dp2: "(Th th3, Th th2) \<in> (depend s)^+" 

      by (simp add:s_dependents_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 cp_rec:

  fixes s th

  assumes vt: "vt step s"

  shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"

proof(unfold cp_eq_cpreced_f cpreced_def)

  let ?f = "(\<lambda>th. preced th s)"

  show "Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th)) =

        Max ({preced th s} \<union> (\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th)"

  proof(cases " children s th = {}")

    case False

    have "(\<lambda>th. Max ((\<lambda>th. preced th s) ` ({th} \<union> dependents (wq s) th))) ` children s th = 

          {Max ((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"

      (is "?L = ?R")

      by auto

    also have "\<dots> = 

      Max ` {((\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th')) | th' . th' \<in> children s th}"

      (is "_ = Max ` ?C")

      by auto

    finally have "Max ?L = Max (Max ` ?C)" by auto

    also have "\<dots> = Max (\<Union> ?C)"

    proof(rule Max_Union[symmetric])

      from children_dependents[of s th] finite_threads[OF vt] and dependents_threads[OF vt, of th]

      show "finite {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"

        by (auto simp:finite_subset)

    next

      from False

      show "{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<noteq> {}"

        by simp

    next

      show "\<And>A. A \<in> {(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th} \<Longrightarrow>

        finite A \<and> A \<noteq> {}"

        apply (auto simp:finite_subset)

      proof -

        fix th'

        from finite_threads[OF vt] and dependents_threads[OF vt, of th']

        show "finite ((\<lambda>th. preced th s) ` dependents (wq s) th')" by (auto simp:finite_subset)

      qed

    qed

    also have "\<dots> = Max ((\<lambda>th. preced th s) ` dependents (wq s) th)"

      (is "Max ?A = Max ?B")

    proof -

      have "?A = ?B"

      proof

        show "\<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}

                    \<subseteq> (\<lambda>th. preced th s) ` dependents (wq s) th"

        proof

          fix x 

          assume "x \<in> \<Union>{(\<lambda>th. preced th s) ` ({th'} \<union> dependents (wq s) th') |th'. th' \<in> children s th}"

          then obtain th' where 

             th'_in: "th' \<in> children s th"

            and x_in: "x \<in> ?f ` ({th'} \<union> dependents (wq s) th')" by auto

          hence "x = ?f th' \<or> x \<in> (?f ` dependents (wq s) th')" by auto

          thus "x \<in> ?f ` dependents (wq s) th"

          proof

            assume "x = preced th' s"

            with th'_in and children_dependents