theory CpsG

imports PIPDefs 

begin

(* I am going to use this file as a start point to retrofiting 

   PIPBasics.thy, which is originally called CpsG.ghy *)

locale valid_trace = 

  fixes s

  assumes vt : "vt s"

locale valid_trace_e = valid_trace +

  fixes e

  assumes vt_e: "vt (e#s)"

begin

lemma pip_e: "PIP s e"

  using vt_e by (cases, simp)  

end

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 [simp]:

   "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 runing_head:

  assumes "th \<in> runing s"

  and "th \<in> set (wq_fun (schs s) cs)"

  shows "th = hd (wq_fun (schs s) cs)"

  using assms

  by (simp add:runing_def readys_def s_waiting_def wq_def)

context valid_trace

begin

lemma actor_inv: 

  assumes "PIP s e"

  and "\<not> isCreate e"

  shows "actor e \<in> runing s"

  using assms

  by (induct, auto)

lemma isP_E:

  assumes "isP e"

  obtains cs where "e = P (actor e) cs"

  using assms by (cases e, auto)

lemma isV_E:

  assumes "isV e"

  obtains cs where "e = V (actor e) cs"

  using assms by (cases e, auto) 

lemma ind [consumes 0, case_names Nil Cons, induct type]:

  assumes "PP []"

     and "(\<And>s e. valid_trace s \<Longrightarrow> valid_trace (e#s) \<Longrightarrow>

                   PP s \<Longrightarrow> PIP s e \<Longrightarrow> PP (e # s))"

     shows "PP s"

proof(rule vt.induct[OF vt])

  from assms(1) show "PP []" .

next

  fix s e

  assume h: "vt s" "PP s" "PIP s e"

  show "PP (e # s)"

  proof(cases rule:assms(2))

    from h(1) show v1: "valid_trace s" by (unfold_locales, simp)

  next

    from h(1,3) have "vt (e#s)" by auto

    thus "valid_trace (e # s)" by (unfold_locales, simp)

  qed (insert h, auto)

qed

lemma wq_distinct: "distinct (wq s cs)"

proof(induct rule:ind)

  case (Cons s e)

  from Cons(4,3)

  show ?case 

  proof(induct)

    case (thread_P th s cs1)

    show ?case 

    proof(cases "cs = cs1")

      case True

      thus ?thesis (is "distinct ?L")

      proof - 

        have "?L = wq_fun (schs s) cs1 @ [th]" using True

          by (simp add:wq_def wf_def Let_def split:list.splits)

        moreover have "distinct ..."

        proof -

          have "th \<notin> set (wq_fun (schs s) cs1)"

          proof

            assume otherwise: "th \<in> set (wq_fun (schs s) cs1)"

            from runing_head[OF thread_P(1) this]

            have "th = hd (wq_fun (schs s) cs1)" .

            hence "(Cs cs1, Th th) \<in> (RAG s)" using otherwise

              by (simp add:s_RAG_def s_holding_def wq_def cs_holding_def)

            with thread_P(2) show False by auto

          qed

          moreover have "distinct (wq_fun (schs s) cs1)"

              using True thread_P wq_def by auto 

          ultimately show ?thesis by auto

        qed

        ultimately show ?thesis by simp

      qed

    next

      case False

      with thread_P(3)

      show ?thesis

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

    qed

  next

    case (thread_V th s cs1)

    thus ?case

    proof(cases "cs = cs1")

      case True

      show ?thesis (is "distinct ?L")

      proof(cases "(wq s cs)")

        case Nil

        thus ?thesis

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

      next

        case (Cons w_hd w_tl)

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

        proof(rule someI2)

          from thread_V(3)[unfolded Cons]

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

        qed auto

        ultimately show ?thesis

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

      qed 

    next

      case False

      with thread_V(3)

      show ?thesis

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

    qed

  qed (insert Cons, auto simp: wq_def Let_def split:list.splits)

qed (unfold wq_def Let_def, simp)

end

context valid_trace_e

begin

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 wq_in_inv: 

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

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

  shows "e = P thread cs"

proof(cases e)

  -- {* This is the only non-trivial case: *}

  case (V th cs1)

  have False

  proof(cases "cs1 = cs")

    case True

    show ?thesis

    proof(cases "(wq s cs1)")

      case (Cons w_hd w_tl)

      have "set (wq (e#s) cs) \<subseteq> set (wq s cs)"

      proof -

        have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)"

          using  Cons V by (auto simp:wq_def Let_def True split:if_splits)

        moreover have "set ... \<subseteq> set (wq s cs)"

        proof(rule someI2)

          show "distinct w_tl \<and> set w_tl = set w_tl"

            by (metis distinct.simps(2) local.Cons wq_distinct)

        qed (insert Cons True, auto)

        ultimately show ?thesis by simp

      qed

      with assms show ?thesis by auto

    qed (insert assms V True, auto simp:wq_def Let_def split:if_splits)

  qed (insert assms V, auto simp:wq_def Let_def split:if_splits)

  thus ?thesis by auto

qed (insert assms, auto simp:wq_def Let_def split:if_splits)

lemma wq_out_inv: 

  assumes s_in: "thread \<in> set (wq s cs)"

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

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

  shows "e = V thread cs"

proof(cases e)

-- {* There are only two non-trivial cases: *}

  case (V th cs1)

  show ?thesis

  proof(cases "cs1 = cs")

    case True

    have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] .

    thus ?thesis

    proof(cases)

      case (thread_V)

      moreover have "th = thread" using thread_V(2) s_hd

          by (unfold s_holding_def wq_def, simp)

      ultimately show ?thesis using V True by simp

    qed

  qed (insert assms V, auto simp:wq_def Let_def split:if_splits)

next

  case (P th cs1)

  show ?thesis

  proof(cases "cs1 = cs")

    case True

    with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]"

      by (auto simp:wq_def Let_def split:if_splits)

    with s_i s_hd s_in have False

      by (metis empty_iff hd_append2 list.set(1) wq_def) 

    thus ?thesis by simp

  qed (insert assms P, auto simp:wq_def Let_def split:if_splits)

qed (insert assms, auto simp:wq_def Let_def split:if_splits)

end

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:

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

context valid_trace_e

begin

lemma abs2:

  assumes 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 vt_e 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 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 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

end

context valid_trace

begin

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

proof(induct rule:ind)

  case Nil

  thus ?case by (simp add:vt_nil)

next

  case (Cons s e t)

  show ?case

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

    case True

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

    thus ?thesis using Cons

      by (simp add:valid_trace_def)

  next

    case False

    from Cons have "vt (moment t s)" by simp

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

    proof -

      from False have "t \<le> length s" by simp

      from moment_app [OF this, of "[e]"] 

      show ?thesis by simp

    qed

    ultimately show ?thesis by simp

  qed

qed

end

locale valid_moment = valid_trace + 

  fixes i :: nat

sublocale valid_moment < vat_moment: valid_trace "(moment i s)"

  by (unfold_locales, insert vt_moment, auto)

context valid_trace

begin

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 lost 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: (* ccc *)

  assumes 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" = "\<lambda> 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> ?Q cs1 (moment t1 s)"

    and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))" by auto

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

  obtain t2 where lt2: "t2 < length s"

    and np2: "\<not> ?Q cs2 (moment t2 s)"

    and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))" by auto

  { fix s cs

    assume q: "?Q cs s"

    have "thread \<notin> runing s"

    proof

      assume "thread \<in> runing s"

      hence " \<forall>cs. \<not> (thread \<in> set (wq_fun (schs s) cs) \<and> 

                 thread \<noteq> hd (wq_fun (schs s) cs))"

        by (unfold runing_def s_waiting_def readys_def, auto)

      from this[rule_format, of cs] q 

      show False by (simp add: wq_def) 

    qed

  } note q_not_runing = this

  { fix i1 i2

    let ?i3 = "Suc i2"

    assume lt12: "i1 < i2"

    and "i1 < length s" "i2 < length s"

    hence le_i3: "?i3 \<le> length s" by auto

    from moment_plus [OF this]

    obtain e where eq_m: "moment ?i3 s = e#moment i2 s" by auto

    have "i2 < ?i3" 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#moment t2 s)"

      proof -

        from vt_moment 

        have "vt (moment ?t3 s)" .

        with eq_m show ?thesis by simp

      qed

      then interpret vt_e: valid_trace_e "moment t2 s" "e"

        by (unfold_locales, auto, cases, simp)

      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 

        from vt_e.abs2 [OF True eq_th h2 h1]

        show ?thesis by auto

      next

        case False

        from vt_e.block_pre[OF False h1]

        have "e = P thread cs2" .

        with vt_e.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

  }

  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#moment t2 s)"

      proof -

        from vt_moment 

        have "vt (moment ?t3 s)" .

        with eq_m show ?thesis by simp

      qed

      then interpret vt_e: valid_trace_e "moment t2 s" "e"

        by (unfold_locales, auto, cases, simp)

      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 

        from vt_e.abs2 [OF True eq_th h2 h1]

        show ?thesis by auto

      next

        case False

        from vt_e.block_pre[OF False h1]

        have "e = P thread cs2" .

        with vt_e.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#moment t1 s)"

      proof -

        from vt_moment

        have "vt (moment ?t3 s)" .

        with eq_m show ?thesis by simp

      qed

      then interpret vt_e: valid_trace_e "moment t1 s" e