theory PrioG

imports PrioGDef 

begin

lemma runing_ready: 

  shows "runing s \<subseteq> readys s"

  unfolding runing_def readys_def

  by auto 

lemma readys_threads:

  shows "readys s \<subseteq> threads s"

  unfolding readys_def

  by auto

lemma wq_v_neq:

   "cs \<noteq> cs' \<Longrightarrow> wq (V thread cs#s) cs' = wq s cs'"

  by (auto simp:wq_def Let_def cp_def split:list.splits)

lemma wq_distinct: "vt s \<Longrightarrow> distinct (wq s cs)"

proof(erule_tac vt.induct, simp add:wq_def)

  fix s e

  assume h1: "step s e"

  and h2: "distinct (wq s cs)"

  thus "distinct (wq (e # s) cs)"

  proof(induct rule:step.induct, auto simp: wq_def Let_def split:list.splits)

    fix thread s

    assume h1: "(Cs cs, Th thread) \<notin> (RAG s)\<^sup>+"

      and h2: "thread \<in> set (wq_fun (schs s) cs)"

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

    show "False" 

    proof -

      from h3 have "\<And> cs. thread \<in>  set (wq_fun (schs s) cs) \<Longrightarrow> 

                             thread = hd ((wq_fun (schs s) cs))" 

        by (simp add:runing_def readys_def s_waiting_def wq_def)

      from this [OF h2] have "thread = hd (wq_fun (schs s) cs)" .

      with h2

      have "(Cs cs, Th thread) \<in> (RAG s)"

        by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)

      with h1 show False by auto

    qed

  next

    fix thread s a list

    assume dst: "distinct list"

    show "distinct (SOME q. distinct q \<and> set q = set list)"

    proof(rule someI2)

      from dst show  "distinct list \<and> set list = set list" by auto

    next

      fix q assume "distinct q \<and> set q = set list"

      thus "distinct q" by auto

    qed

  qed

qed

text {*

  The following lemma shows that only the @{text "P"}

  operation can add new thread into waiting queues. 

  Such kind of lemmas are very obvious, but need to be checked formally.

  This is a kind of confirmation that our modelling is correct.

*}

lemma block_pre: 

  fixes thread cs s

  assumes vt_e: "vt (e#s)"

  and s_ni: "thread \<notin>  set (wq s cs)"

  and s_i: "thread \<in> set (wq (e#s) cs)"

  shows "e = P thread cs"

proof -

  show ?thesis

  proof(cases e)

    case (P th cs)

    with assms

    show ?thesis

      by (auto simp:wq_def Let_def split:if_splits)

  next

    case (Create th prio)

    with assms show ?thesis

      by (auto simp:wq_def Let_def split:if_splits)

  next

    case (Exit th)

    with assms show ?thesis

      by (auto simp:wq_def Let_def split:if_splits)

  next

    case (Set th prio)

    with assms show ?thesis

      by (auto simp:wq_def Let_def split:if_splits)

  next

    case (V th cs)

    with assms show ?thesis

      apply (auto simp:wq_def Let_def split:if_splits)

    proof -

      fix q qs

      assume h1: "thread \<notin> set (wq_fun (schs s) cs)"

        and h2: "q # qs = wq_fun (schs s) cs"

        and h3: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"

        and vt: "vt (V th cs # s)"

      from h1 and h2[symmetric] have "thread \<notin> set (q # qs)" by simp

      moreover have "thread \<in> set qs"

      proof -

        have "set (SOME q. distinct q \<and> set q = set qs) = set qs"

        proof(rule someI2)

          from wq_distinct [OF step_back_vt[OF vt], of cs]

          and h2[symmetric, folded wq_def]

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

        next

          fix x assume "distinct x \<and> set x = set qs"

          thus "set x = set qs" by auto

        qed

        with h3 show ?thesis by simp

      qed

      ultimately show "False" by auto

      qed

  qed

qed

text {*

  The following lemmas is also obvious and shallow. It says

  that only running thread can request for a critical resource 

  and that the requested resource must be one which is

  not current held by the thread.

*}

lemma p_pre: "\<lbrakk>vt ((P thread cs)#s)\<rbrakk> \<Longrightarrow> 

  thread \<in> runing s \<and> (Cs cs, Th thread)  \<notin> (RAG s)^+"

apply (ind_cases "vt ((P thread cs)#s)")

apply (ind_cases "step s (P thread cs)")

by auto

lemma abs1:

  fixes e es

  assumes ein: "e \<in> set es"

  and neq: "hd es \<noteq> hd (es @ [x])"

  shows "False"

proof -

  from ein have "es \<noteq> []" by auto

  then obtain e ess where "es = e # ess" by (cases es, auto)

  with neq show ?thesis by auto

qed

lemma q_head: "Q (hd es) \<Longrightarrow> hd es = hd [th\<leftarrow>es . Q th]"

  by (cases es, auto)

inductive_cases evt_cons: "vt (a#s)"

lemma abs2:

  assumes vt: "vt (e#s)"

  and inq: "thread \<in> set (wq s cs)"

  and nh: "thread = hd (wq s cs)"

  and qt: "thread \<noteq> hd (wq (e#s) cs)"

  and inq': "thread \<in> set (wq (e#s) cs)"

  shows "False"

proof -

  from assms show "False"

    apply (cases e)

    apply ((simp split:if_splits add:Let_def wq_def)[1])+

    apply (insert abs1, fast)[1]

    apply (auto simp:wq_def simp:Let_def split:if_splits list.splits)

  proof -

    fix th qs

    assume vt: "vt (V th cs # s)"

      and th_in: "thread \<in> set (SOME q. distinct q \<and> set q = set qs)"

      and eq_wq: "wq_fun (schs s) cs = thread # qs"

    show "False"

    proof -

      from wq_distinct[OF step_back_vt[OF vt], of cs]

        and eq_wq[folded wq_def] have "distinct (thread#qs)" by simp

      moreover have "thread \<in> set qs"

      proof -

        have "set (SOME q. distinct q \<and> set q = set qs) = set qs"

        proof(rule someI2)

          from wq_distinct [OF step_back_vt[OF vt], of cs]

          and eq_wq [folded wq_def]

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

        next

          fix x assume "distinct x \<and> set x = set qs"

          thus "set x = set qs" by auto

        qed

        with th_in show ?thesis by auto

      qed

      ultimately show ?thesis by auto

    qed

  qed

qed

lemma vt_moment: "\<And> t. \<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"

proof(induct s, simp)

  fix a s t

  assume h: "\<And>t.\<lbrakk>vt s\<rbrakk> \<Longrightarrow> vt (moment t s)"

    and vt_a: "vt (a # s)"

  show "vt (moment t (a # s))"

  proof(cases "t \<ge> length (a#s)")

    case True

    from True have "moment t (a#s) = a#s" by simp

    with vt_a show ?thesis by simp

  next

    case False

    hence le_t1: "t \<le> length s" by simp

    from vt_a have "vt s"

      by (erule_tac evt_cons, simp)

    from h [OF this] have "vt (moment t s)" .

    moreover have "moment t (a#s) = moment t s"

    proof -

      from moment_app [OF le_t1, of "[a]"] 

      show ?thesis by simp

    qed

    ultimately show ?thesis by auto

  qed

qed

(* Wrong:

    lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"

*)

text {* (* ddd *)

  The nature of the work is like this: since it starts from a very simple and basic 

  model, even intuitively very `basic` and `obvious` properties need to derived from scratch.

  For instance, the fact 

  that one thread can not be blocked by two critical resources at the same time

  is obvious, because only running threads can make new requests, if one is waiting for 

  a critical resource and get blocked, it can not make another resource request and get 

  blocked the second time (because it is not running). 

  To derive this fact, one needs to prove by contraction and 

  reason about time (or @{text "moement"}). The reasoning is based on a generic theorem

  named @{text "p_split"}, which is about status changing along the time axis. It says if 

  a condition @{text "Q"} is @{text "True"} at a state @{text "s"},

  but it was @{text "False"} at the very beginning, then there must exits a moment @{text "t"} 

  in the history of @{text "s"} (notice that @{text "s"} itself is essentially the history 

  of events leading to it), such that @{text "Q"} switched 

  from being @{text "False"} to @{text "True"} and kept being @{text "True"}

  till the last moment of @{text "s"}.

  Suppose a thread @{text "th"} is blocked

  on @{text "cs1"} and @{text "cs2"} in some state @{text "s"}, 

  since no thread is blocked at the very beginning, by applying 

  @{text "p_split"} to these two blocking facts, there exist 

  two moments @{text "t1"} and @{text "t2"}  in @{text "s"}, such that 

  @{text "th"} got blocked on @{text "cs1"} and @{text "cs2"} 

  and kept on blocked on them respectively ever since.

  Without lose of generality, we assume @{text "t1"} is earlier than @{text "t2"}.

  However, since @{text "th"} was blocked ever since memonent @{text "t1"}, so it was still

  in blocked state at moment @{text "t2"} and could not

  make any request and get blocked the second time: Contradiction.

*}

lemma waiting_unique_pre:

  fixes cs1 cs2 s thread

  assumes vt: "vt s"

  and h11: "thread \<in> set (wq s cs1)"

  and h12: "thread \<noteq> hd (wq s cs1)"

  assumes h21: "thread \<in> set (wq s cs2)"

  and h22: "thread \<noteq> hd (wq s cs2)"

  and neq12: "cs1 \<noteq> cs2"

  shows "False"

proof -

  let "?Q cs s" = "thread \<in> set (wq s cs) \<and> thread \<noteq> hd (wq s cs)"

  from h11 and h12 have q1: "?Q cs1 s" by simp

  from h21 and h22 have q2: "?Q cs2 s" by simp

  have nq1: "\<not> ?Q cs1 []" by (simp add:wq_def)

  have nq2: "\<not> ?Q cs2 []" by (simp add:wq_def)

  from p_split [of "?Q cs1", OF q1 nq1]

  obtain t1 where lt1: "t1 < length s"

    and np1: "\<not>(thread \<in> set (wq (moment t1 s) cs1) \<and>

        thread \<noteq> hd (wq (moment t1 s) cs1))"

    and nn1: "(\<forall>i'>t1. thread \<in> set (wq (moment i' s) cs1) \<and>

             thread \<noteq> hd (wq (moment i' s) cs1))" by auto

  from p_split [of "?Q cs2", OF q2 nq2]

  obtain t2 where lt2: "t2 < length s"

    and np2: "\<not>(thread \<in> set (wq (moment t2 s) cs2) \<and>

        thread \<noteq> hd (wq (moment t2 s) cs2))"

    and nn2: "(\<forall>i'>t2. thread \<in> set (wq (moment i' s) cs2) \<and>

             thread \<noteq> hd (wq (moment i' s) cs2))" by auto

  show ?thesis

  proof -

    { 

      assume lt12: "t1 < t2"

      let ?t3 = "Suc t2"

      from lt2 have le_t3: "?t3 \<le> length s" by auto

      from moment_plus [OF this] 

      obtain e where eq_m: "moment ?t3 s = e#moment t2 s" by auto

      have "t2 < ?t3" by simp

      from nn2 [rule_format, OF this] and eq_m

      have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and

        h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto

      have vt_e: "vt (e#moment t2 s)"

      proof -

        from vt_moment [OF vt]

        have "vt (moment ?t3 s)" .

        with eq_m show ?thesis by simp

      qed

      have ?thesis

      proof(cases "thread \<in> set (wq (moment t2 s) cs2)")

        case True

        from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"

          by auto

          thm abs2

        from abs2 [OF vt_e True eq_th h2 h1]

        show ?thesis by auto

      next

        case False

        from block_pre [OF vt_e False h1]

        have "e = P thread cs2" .

        with vt_e have "vt ((P thread cs2)# moment t2 s)" by simp

        from p_pre [OF this] have "thread \<in> runing (moment t2 s)" by simp

        with runing_ready have "thread \<in> readys (moment t2 s)" by auto

        with nn1 [rule_format, OF lt12]

        show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)

      qed

    } moreover {

      assume lt12: "t2 < t1"

      let ?t3 = "Suc t1"

      from lt1 have le_t3: "?t3 \<le> length s" by auto

      from moment_plus [OF this] 

      obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto

      have lt_t3: "t1 < ?t3" by simp

      from nn1 [rule_format, OF this] and eq_m

      have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and

        h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto

      have vt_e: "vt  (e#moment t1 s)"

      proof -

        from vt_moment [OF vt]

        have "vt (moment ?t3 s)" .

        with eq_m show ?thesis by simp

      qed

      have ?thesis

      proof(cases "thread \<in> set (wq (moment t1 s) cs1)")

        case True

        from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"

          by auto

        from abs2 [OF vt_e True eq_th h2 h1]

        show ?thesis by auto

      next

        case False

        from block_pre [OF vt_e False h1]

        have "e = P thread cs1" .

        with vt_e have "vt ((P thread cs1)# moment t1 s)" by simp

        from p_pre [OF this] have "thread \<in> runing (moment t1 s)" by simp

        with runing_ready have "thread \<in> readys (moment t1 s)" by auto

        with nn2 [rule_format, OF lt12]

        show ?thesis  by (simp add:readys_def wq_def s_waiting_def, auto)

      qed

    } moreover {

      assume eqt12: "t1 = t2"

      let ?t3 = "Suc t1"

      from lt1 have le_t3: "?t3 \<le> length s" by auto

      from moment_plus [OF this] 

      obtain e where eq_m: "moment ?t3 s = e#moment t1 s" by auto

      have lt_t3: "t1 < ?t3" by simp

      from nn1 [rule_format, OF this] and eq_m

      have h1: "thread \<in> set (wq (e#moment t1 s) cs1)" and

        h2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" by auto

      have vt_e: "vt (e#moment t1 s)"

      proof -

        from vt_moment [OF vt]

        have "vt (moment ?t3 s)" .

        with eq_m show ?thesis by simp

      qed

      have ?thesis

      proof(cases "thread \<in> set (wq (moment t1 s) cs1)")

        case True

        from True and np1 have eq_th: "thread = hd (wq (moment t1 s) cs1)"

          by auto

        from abs2 [OF vt_e True eq_th h2 h1]

        show ?thesis by auto

      next

        case False

        from block_pre [OF vt_e False h1]

        have eq_e1: "e = P thread cs1" .

        have lt_t3: "t1 < ?t3" by simp

        with eqt12 have "t2 < ?t3" by simp

        from nn2 [rule_format, OF this] and eq_m and eqt12

        have h1: "thread \<in> set (wq (e#moment t2 s) cs2)" and

          h2: "thread \<noteq> hd (wq (e#moment t2 s) cs2)" by auto

        show ?thesis

        proof(cases "thread \<in> set (wq (moment t2 s) cs2)")

          case True

          from True and np2 have eq_th: "thread = hd (wq (moment t2 s) cs2)"

            by auto

          from vt_e and eqt12 have "vt (e#moment t2 s)" by simp 

          from abs2 [OF this True eq_th h2 h1]

          show ?thesis .

        next

          case False

          have vt_e: "vt (e#moment t2 s)"

          proof -

            from vt_moment [OF vt] eqt12

            have "vt (moment (Suc t2) s)" by auto

            with eq_m eqt12 show ?thesis by simp

          qed

          from block_pre [OF vt_e False h1]

          have "e = P thread cs2" .

          with eq_e1 neq12 show ?thesis by auto

        qed

      qed

    } ultimately show ?thesis by arith

  qed

qed

text {*

  This lemma is a simple corrolary of @{text "waiting_unique_pre"}.

*}

lemma waiting_unique:

  fixes s cs1 cs2

  assumes "vt s"

  and "waiting s th cs1"

  and "waiting s th cs2"

  shows "cs1 = cs2"

using waiting_unique_pre assms

unfolding wq_def s_waiting_def

by auto

(* not used *)

text {*

  Every thread can only be blocked on one critical resource, 

  symmetrically, every critical resource can only be held by one thread. 

  This fact is much more easier according to our definition. 

*}

lemma held_unique:

  fixes s::"state"

  assumes "holding s th1 cs"

  and "holding s th2 cs"

  shows "th1 = th2"

using assms

unfolding s_holding_def

by auto

lemma last_set_lt: "th \<in> threads s \<Longrightarrow> last_set th s < length s"

  apply (induct s, auto)

  by (case_tac a, auto split:if_splits)

lemma last_set_unique: 

  "\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>

          \<Longrightarrow> th1 = th2"

  apply (induct s, auto)

  by (case_tac a, auto split:if_splits dest:last_set_lt)

lemma preced_unique : 

  assumes pcd_eq: "preced th1 s = preced th2 s"

  and th_in1: "th1 \<in> threads s"

  and th_in2: " th2 \<in> threads s"

  shows "th1 = th2"

proof -

  from pcd_eq have "last_set th1 s = last_set th2 s" by (simp add:preced_def)

  from last_set_unique [OF this th_in1 th_in2]

  show ?thesis .

qed

lemma preced_linorder: 

  assumes neq_12: "th1 \<noteq> th2"

  and th_in1: "th1 \<in> threads s"

  and th_in2: " th2 \<in> threads s"

  shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"

proof -

  from preced_unique [OF _ th_in1 th_in2] and neq_12 

  have "preced th1 s \<noteq> preced th2 s" by auto

  thus ?thesis by auto

qed

(* An aux lemma used later *)

lemma unique_minus:

  fixes x y z r

  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

  and xy: "(x, y) \<in> r"

  and xz: "(x, z) \<in> r^+"

  and neq: "y \<noteq> z"

  shows "(y, z) \<in> r^+"

proof -

 from xz and neq show ?thesis

 proof(induct)

   case (base ya)

   have "(x, ya) \<in> r" by fact

   from unique [OF xy this] have "y = ya" .

   with base show ?case by auto

 next

   case (step ya z)

   show ?case

   proof(cases "y = ya")

     case True

     from step True show ?thesis by simp

   next

     case False

     from step False

     show ?thesis by auto

   qed

 qed

qed

lemma unique_base:

  fixes r x y z

  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

  and xy: "(x, y) \<in> r"

  and xz: "(x, z) \<in> r^+"

  and neq_yz: "y \<noteq> z"

  shows "(y, z) \<in> r^+"

proof -

  from xz neq_yz show ?thesis

  proof(induct)

    case (base ya)

    from xy unique base show ?case by auto

  next

    case (step ya z)

    show ?case

    proof(cases "y = ya")

      case True

      from True step show ?thesis by auto

    next

      case False

      from False step 

      have "(y, ya) \<in> r\<^sup>+" by auto

      with step show ?thesis by auto

    qed

  qed

qed

lemma unique_chain:

  fixes r x y z

  assumes unique: "\<And> a b c. \<lbrakk>(a, b) \<in> r; (a, c) \<in> r\<rbrakk> \<Longrightarrow> b = c"

  and xy: "(x, y) \<in> r^+"

  and xz: "(x, z) \<in> r^+"

  and neq_yz: "y \<noteq> z"

  shows "(y, z) \<in> r^+ \<or> (z, y) \<in> r^+"

proof -

  from xy xz neq_yz show ?thesis

  proof(induct)

    case (base y)

    have h1: "(x, y) \<in> r" and h2: "(x, z) \<in> r\<^sup>+" and h3: "y \<noteq> z" using base by auto