section {*

  This file contains lemmas used to guide the recalculation of current precedence 

  after every system call (or system operation)

*}

theory CpsG

imports PrioG Max

begin

(* obvious lemma *)

lemma not_thread_holdents:

  fixes th s

  assumes vt: "vt s"

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

  shows "holdents s th = {}"

proof -

  from vt not_in show ?thesis

  proof(induct arbitrary:th)

    case (vt_cons s e th)

    assume vt: "vt s"

      and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"

      and stp: "step s e"

      and not_in: "th \<notin> threads (e # s)"

    from stp show ?case

    proof(cases)

      case (thread_create thread prio)

      assume eq_e: "e = Create thread prio"

        and not_in': "thread \<notin> threads s"

      have "holdents (e # s) th = holdents s th"

        apply (unfold eq_e holdents_test)

        by (simp add:RAG_create_unchanged)

      moreover have "th \<notin> threads s" 

      proof -

        from not_in eq_e show ?thesis by simp

      qed

      moreover note ih ultimately show ?thesis by auto

    next

      case (thread_exit thread)

      assume eq_e: "e = Exit thread"

      and nh: "holdents s thread = {}"

      show ?thesis

      proof(cases "th = thread")

        case True

        with nh eq_e

        show ?thesis 

          by (auto simp:holdents_test RAG_exit_unchanged)

      next

        case False

        with not_in and eq_e

        have "th \<notin> threads s" by simp

        from ih[OF this] False eq_e show ?thesis 

          by (auto simp:holdents_test RAG_exit_unchanged)

      qed

    next

      case (thread_P thread cs)

      assume eq_e: "e = P thread cs"

      and is_runing: "thread \<in> runing s"

      from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto

      have neq_th: "th \<noteq> thread" 

      proof -

        from not_in eq_e have "th \<notin> threads s" by simp

        moreover from is_runing have "thread \<in> threads s"

          by (simp add:runing_def readys_def)

        ultimately show ?thesis by auto

      qed

      hence "holdents (e # s) th  = holdents s th "

        apply (unfold cntCS_def holdents_test eq_e)

        by (unfold step_RAG_p[OF vtp], auto)

      moreover have "holdents s th = {}"

      proof(rule ih)

        from not_in eq_e show "th \<notin> threads s" by simp

      qed

      ultimately show ?thesis by simp

    next

      case (thread_V thread cs)

      assume eq_e: "e = V thread cs"

        and is_runing: "thread \<in> runing s"

        and hold: "holding s thread cs"

      have neq_th: "th \<noteq> thread" 

      proof -

        from not_in eq_e have "th \<notin> threads s" by simp

        moreover from is_runing have "thread \<in> threads s"

          by (simp add:runing_def readys_def)

        ultimately show ?thesis by auto

      qed

      from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto

      from hold obtain rest 

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

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

      from not_in eq_e eq_wq

      have "\<not> next_th s thread cs th"

        apply (auto simp:next_th_def)

      proof -

        assume ne: "rest \<noteq> []"

          and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")

        have "?t \<in> set rest"

        proof(rule someI2)

          from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq

          show "distinct rest \<and> set rest = set rest" by auto

        next

          fix x assume "distinct x \<and> set x = set rest" with ne

          show "hd x \<in> set rest" by (cases x, auto)

        qed

        with eq_wq have "?t \<in> set (wq s cs)" by simp

        from wq_threads[OF step_back_vt[OF vtv], OF this] and ni

        show False by auto

      qed

      moreover note neq_th eq_wq

      ultimately have "holdents (e # s) th  = holdents s th"

        by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)

      moreover have "holdents s th = {}"

      proof(rule ih)

        from not_in eq_e show "th \<notin> threads s" by simp

      qed

      ultimately show ?thesis by simp

    next

      case (thread_set thread prio)

      print_facts

      assume eq_e: "e = Set thread prio"

        and is_runing: "thread \<in> runing s"

      from not_in and eq_e have "th \<notin> threads s" by auto

      from ih [OF this] and eq_e

      show ?thesis 

        apply (unfold eq_e cntCS_def holdents_test)

        by (simp add:RAG_set_unchanged)

    qed

    next

      case vt_nil

      show ?case

      by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)

  qed

qed

(* obvious lemma *)

lemma next_th_neq: 

  assumes vt: "vt s"

  and nt: "next_th s th cs th'"

  shows "th' \<noteq> th"

proof -

  from nt show ?thesis

    apply (auto simp:next_th_def)

  proof -

    fix rest

    assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"

      and ne: "rest \<noteq> []"

    have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" 

    proof(rule someI2)

      from wq_distinct[OF vt, of cs] eq_wq

      show "distinct rest \<and> set rest = set rest" by auto

    next

      fix x

      assume "distinct x \<and> set x = set rest"

      hence eq_set: "set x = set rest" by auto

      with ne have "x \<noteq> []" by auto

      hence "hd x \<in> set x" by auto

      with eq_set show "hd x \<in> set rest" by auto

    qed

    with wq_distinct[OF vt, of cs] eq_wq show False by auto

  qed

qed

(* obvious lemma *)

lemma next_th_unique: 

  assumes nt1: "next_th s th cs th1"

  and nt2: "next_th s th cs th2"

  shows "th1 = th2"

using assms by (unfold next_th_def, auto)

lemma wf_RAG:

  assumes vt: "vt s"

  shows "wf (RAG s)"

proof(rule finite_acyclic_wf)

  from finite_RAG[OF vt] show "finite (RAG s)" .

next

  from acyclic_RAG[OF vt] show "acyclic (RAG s)" .

qed

definition child :: "state \<Rightarrow> (node \<times> node) set"

  where "child s \<equiv>

            {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"

definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"

  where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"

lemma children_def2:

  "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"

unfolding child_def children_def by simp

lemma children_dependants: 

  "children s th \<subseteq> dependants (wq s) th"

  unfolding children_def2

  unfolding cs_dependants_def

  by (auto simp add: eq_RAG)

lemma child_unique:

  assumes vt: "vt s"

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

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

  shows "th1 = th2"

using ch1 ch2 

proof(unfold child_def, clarsimp)

  fix cs csa

  assume h1: "(Th th, Cs cs) \<in> RAG s"

    and h2: "(Cs cs, Th th1) \<in> RAG s"

    and h3: "(Th th, Cs csa) \<in> RAG s"

    and h4: "(Cs csa, Th th2) \<in> RAG s"

  from unique_RAG[OF vt h1 h3] have "cs = csa" by simp

  with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp

  from unique_RAG[OF vt h2 this]

  show "th1 = th2" by simp

qed 

lemma RAG_children:

  assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"

  shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"

proof -

  from h show ?thesis

  proof(induct rule: tranclE)

    fix c th2

    assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"

    and h2: "(c, Th th2) \<in> RAG s"

    from h2 obtain cs where eq_c: "c = Cs cs"

      by (case_tac c, auto simp:s_RAG_def)

    show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"

    proof(rule tranclE[OF h1])

      fix ca

      assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"

        and h4: "(ca, c) \<in> RAG s"

      show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"

      proof -

        from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"

          by (case_tac ca, auto simp:s_RAG_def)

        from eq_ca h4 h2 eq_c

        have "th3 \<in> children s th2" by (auto simp:children_def child_def)

        moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp

        ultimately show ?thesis by auto

      qed

    next

      assume "(Th th1, c) \<in> RAG s"

      with h2 eq_c

      have "th1 \<in> children s th2"

        by (auto simp:children_def child_def)

      thus ?thesis by auto

    qed

  next

    assume "(Th th1, Th th2) \<in> RAG s"

    thus ?thesis

      by (auto simp:s_RAG_def)

  qed

qed

lemma sub_child: "child s \<subseteq> (RAG s)^+"

  by (unfold child_def, auto)

lemma wf_child: 

  assumes vt: "vt s"

  shows "wf (child s)"

apply(rule wf_subset)

apply(rule wf_trancl[OF wf_RAG[OF vt]])

apply(rule sub_child)

done

lemma RAG_child_pre:

  assumes vt: "vt s"

  shows

  "(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")

proof -

  from wf_trancl[OF wf_RAG[OF vt]]

  have wf: "wf ((RAG s)^+)" .

  show ?thesis

  proof(rule wf_induct[OF wf, of ?P], clarsimp)

    fix th'

    assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>

               (Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"

    and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"

    show "(Th th, Th th') \<in> (child s)\<^sup>+"

    proof -

      from RAG_children[OF h]

      have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .

      thus ?thesis

      proof

        assume "th \<in> children s th'"

        thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)

      next

        assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"

        then obtain th3 where th3_in: "th3 \<in> children s th'" 

          and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto

        from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)

        from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp

        with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)

      qed

    qed

  qed

qed

lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"

  by (insert RAG_child_pre, auto)

lemma child_RAG_p:

  assumes "(n1, n2) \<in> (child s)^+"

  shows "(n1, n2) \<in> (RAG s)^+"

proof -

  from assms show ?thesis

  proof(induct)

    case (base y)

    with sub_child show ?case by auto

  next

    case (step y z)

    assume "(y, z) \<in> child s"

    with sub_child have "(y, z) \<in> (RAG s)^+" by auto

    moreover have "(n1, y) \<in> (RAG s)^+" by fact

    ultimately show ?case by auto

  qed

qed

*}

lemma child_RAG_eq: 

  assumes vt: "vt s"

  shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"

  by (auto intro: RAG_child[OF vt] child_RAG_p)

*}

lemma children_no_dep:

  fixes s th th1 th2 th3

  assumes vt: "vt s"

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

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

  and ch3: "(Th th1, Th th2) \<in> (RAG s)^+"

  shows "False"

proof -

  from RAG_child[OF vt ch3]

  have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .

  thus ?thesis

  proof(rule converse_tranclE)

    assume "(Th th1, Th th2) \<in> child s"

    from child_unique[OF vt ch1 this] have "th = th2" by simp

    with ch2 have "(Th th2, Th th2) \<in> child s" by simp

    with wf_child[OF vt] show ?thesis by auto

  next

    fix c

    assume h1: "(Th th1, c) \<in> child s"

      and h2: "(c, Th th2) \<in> (child s)\<^sup>+"

    from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)

    with h1 have "(Th th1, Th th3) \<in> child s" by simp

    from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp

    with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp

    with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto

    moreover have "wf ((child s)\<^sup>+)"

    proof(rule wf_trancl)

      from wf_child[OF vt] show "wf (child s)" .

    qed

    ultimately show False by auto

  qed

qed

*}

lemma unique_RAG_p:

  assumes vt: "vt s"

  and dp1: "(n, n1) \<in> (RAG s)^+"

  and dp2: "(n, n2) \<in> (RAG s)^+"

  and neq: "n1 \<noteq> n2"

  shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"

proof(rule unique_chain [OF _ dp1 dp2 neq])

  from unique_RAG[OF vt]

  show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto

qed

*}

lemma dependants_child_unique:

  fixes s th th1 th2 th3

  assumes vt: "vt s"

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

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

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

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

shows "th1 = th2"

proof -

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

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

      by (simp add:s_dependants_def eq_RAG)

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

      by (simp add:s_dependants_def eq_RAG)

    from unique_RAG_p[OF vt dp1 dp2] and neq

    have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto

    hence False

    proof

      assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ "

      from children_no_dep[OF vt ch1 ch2 this] show ?thesis .

    next

      assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"

      from children_no_dep[OF vt ch2 ch1 this] show ?thesis .

    qed

  } thus ?thesis by auto

qed

lemma RAG_plus_elim:

  assumes "vt s"

  fixes x

  assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"

  shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"

  using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]

  apply (unfold children_def)

  by (metis assms(2) children_def RAG_children eq_RAG)

*}

lemma dependants_expand:

  assumes "vt s"

  shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"

apply(simp add: image_def)

unfolding cs_dependants_def

apply(auto)

apply (metis assms RAG_plus_elim mem_Collect_eq)

apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')

by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)

lemma finite_children:

  assumes "vt s"

  shows "finite (children s th)"

  using children_dependants dependants_threads[OF assms] finite_threads[OF assms]

  by (metis rev_finite_subset)

lemma finite_dependants:

  assumes "vt s"

  shows "finite (dependants (wq s) th')"

  using dependants_threads[OF assms] finite_threads[OF assms]

  by (metis rev_finite_subset)

abbreviation

  "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"

abbreviation

  "cpreceds s ths \<equiv> (cp s) ` ths"

lemma Un_compr:

  "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"

by auto

lemma in_disj:

  shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"

by metis

lemma UN_exists:

  shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"

by auto

*}

lemma cp_rec:

  fixes s th

  assumes vt: "vt s"

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

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

  case True

  show ?thesis

    unfolding cp_eq_cpreced cpreced_def 

    by (subst dependants_expand[OF `vt s`]) (simp add: True)

next

  case False

  show ?thesis (is "?LHS = ?RHS")

  proof -

    have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"

      by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])

    have not_emptyness_facts[simp]: 

      "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"

      using False dependants_expand[OF assms] by(auto simp only: Un_empty)

    have finiteness_facts[simp]:

      "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"

      by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])

    (* expanding definition *)

    have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"

      unfolding eq_cp by (simp add: Un_compr)

    (* moving Max in *)

    also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"

      by (simp add: Max_Un)

    (* expanding dependants *)

    also have "\<dots> = max (Max {preced th s}) 

      (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"

      by (subst dependants_expand[OF `vt s`]) (simp)

    (* moving out big Union *)

    also have "\<dots> = max (Max {preced th s})

      (Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"  

      by simp

    (* moving in small union *)

    also have "\<dots> = max (Max {preced th s})

      (Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"  

      by (simp add: in_disj)

    (* moving in preceds *)