theory CpsG

imports PIPDefs 

begin

lemma Max_f_mono:

  assumes seq: "A \<subseteq> B"

  and np: "A \<noteq> {}"

  and fnt: "finite B"

  shows "Max (f ` A) \<le> Max (f ` B)"

proof(rule Max_mono)

  from seq show "f ` A \<subseteq> f ` B" by auto

next

  from np show "f ` A \<noteq> {}" by auto

next

  from fnt and seq show "finite (f ` B)" by auto

qed

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

locale valid_trace_create = valid_trace_e + 

  fixes th prio

  assumes is_create: "e = Create th prio"

locale valid_trace_exit = valid_trace_e + 

  fixes th

  assumes is_exit: "e = Exit th"

locale valid_trace_p = valid_trace_e + 

  fixes th cs

  assumes is_p: "e = P th cs"

locale valid_trace_v = valid_trace_e + 

  fixes th cs

  assumes is_v: "e = V th cs"

begin

  definition "rest = tl (wq s cs)"

  definition "wq' = (SOME q. distinct q \<and> set q = set rest)"

end

locale valid_trace_v_n = valid_trace_v +

  assumes rest_nnl: "rest \<noteq> []"

locale valid_trace_v_e = valid_trace_v +

  assumes rest_nil: "rest = []"

locale valid_trace_set= valid_trace_e + 

  fixes th prio

  assumes is_set: "e = Set th prio"

context valid_trace

begin

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

  assumes "PP []"

     and "(\<And>s e. valid_trace_e s e \<Longrightarrow>

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

     shows "PP s"

proof(induct rule:vt.induct[OF vt, case_names Init Step])

  case Init

  from assms(1) show ?case .

next

  case (Step s e)

  show ?case

  proof(rule assms(2))

    show "valid_trace_e s e" using Step by (unfold_locales, auto)

  next

    show "PP s" using Step by simp

  next

    show "PIP s e" using Step by simp

  qed

qed

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 valid_trace_e_def, auto)

  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

lemma finite_threads:

  shows "finite (threads s)"

using vt by (induct) (auto elim: step.cases)

end

lemma cp_eq_cpreced: "cp s th = cpreced (wq s) s th"

unfolding cp_def wq_def

apply(induct s rule: schs.induct)

apply(simp add: Let_def cpreced_initial)

apply(simp add: Let_def)

apply(simp add: Let_def)

apply(simp add: Let_def)

apply(subst (2) schs.simps)

apply(simp add: Let_def)

apply(subst (2) schs.simps)

apply(simp add: Let_def)

done

lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"

  by (unfold s_RAG_def, auto)

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)

lemma waiting_eq: "waiting s th cs = waiting (wq s) th cs"

  by  (unfold s_waiting_def cs_waiting_def wq_def, auto)

lemma holding_eq: "holding (s::state) th cs = holding (wq s) th cs"

  by (unfold s_holding_def wq_def cs_holding_def, simp)

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

  assumes "th \<in> runing s"

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

  obtains rest where "wq s cs = th#rest"

proof -

  from assms(2) obtain th' rest where eq_wq: "wq s cs = th'#rest"

    by (meson list.set_cases)

  have "th' = th"

  proof(rule ccontr)

    assume "th' \<noteq> th"

    hence "th \<noteq> hd (wq s cs)" using eq_wq by auto 

    with assms(2)

    have "waiting s th cs" 

      by (unfold s_waiting_def, fold wq_def, auto)

    with assms show False 

      by (unfold runing_def readys_def, auto)

  qed

  with eq_wq that show ?thesis by metis

qed

end

context valid_trace_create

begin

lemma wq_neq_simp [simp]:

  shows "wq (e#s) cs' = wq s cs'"

    using assms unfolding is_create wq_def

  by (auto simp:Let_def)

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

  shows "distinct (wq (e#s) cs')"

  using assms by simp

end

context valid_trace_exit

begin

lemma wq_neq_simp [simp]:

  shows "wq (e#s) cs' = wq s cs'"

    using assms unfolding is_exit wq_def

  by (auto simp:Let_def)

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

  shows "distinct (wq (e#s) cs')"

  using assms by simp

end

context valid_trace_p

begin

lemma wq_neq_simp [simp]:

  assumes "cs' \<noteq> cs"

  shows "wq (e#s) cs' = wq s cs'"

    using assms unfolding is_p wq_def

  by (auto simp:Let_def)

lemma runing_th_s:

  shows "th \<in> runing s"

proof -

  from pip_e[unfolded is_p]

  show ?thesis by (cases, simp)

qed

lemma th_not_waiting: 

  "\<not> waiting s th c"

proof -

  have "th \<in> readys s"

    using runing_ready runing_th_s by blast 

  thus ?thesis

    by (unfold readys_def, auto)

qed

lemma waiting_neq_th: 

  assumes "waiting s t c"

  shows "t \<noteq> th"

  using assms using th_not_waiting by blast 

lemma th_not_in_wq: 

  shows "th \<notin> set (wq s cs)"

proof

  assume otherwise: "th \<in> set (wq s cs)"

  from runing_wqE[OF runing_th_s this]

  obtain rest where eq_wq: "wq s cs = th#rest" by blast

  with otherwise

  have "holding s th cs"

    by (unfold s_holding_def, fold wq_def, simp)

  hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s"

    by (unfold s_RAG_def, fold holding_eq, auto)

  from pip_e[unfolded is_p]

  show False

  proof(cases)

    case (thread_P)

    with cs_th_RAG show ?thesis by auto

  qed

qed

lemma wq_es_cs: 

  "wq (e#s) cs =  wq s cs @ [th]"

  by (unfold is_p wq_def, auto simp:Let_def)

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

  shows "distinct (wq (e#s) cs')"

proof(cases "cs' = cs")

  case True

  show ?thesis using True assms th_not_in_wq

    by (unfold True wq_es_cs, auto)

qed (insert assms, simp)

end

context valid_trace_v

begin

lemma wq_neq_simp [simp]:

  assumes "cs' \<noteq> cs"

  shows "wq (e#s) cs' = wq s cs'"

    using assms unfolding is_v wq_def

  by (auto simp:Let_def)

lemma runing_th_s:

  shows "th \<in> runing s"

proof -

  from pip_e[unfolded is_v]

  show ?thesis by (cases, simp)

qed

lemma th_not_waiting: 

  "\<not> waiting s th c"

proof -

  have "th \<in> readys s"

    using runing_ready runing_th_s by blast 

  thus ?thesis

    by (unfold readys_def, auto)

qed

lemma waiting_neq_th: 

  assumes "waiting s t c"

  shows "t \<noteq> th"

  using assms using th_not_waiting by blast 

lemma wq_s_cs:

  "wq s cs = th#rest"

proof -

  from pip_e[unfolded is_v]

  show ?thesis

  proof(cases)

    case (thread_V)

    from this(2) show ?thesis

      by (unfold rest_def s_holding_def, fold wq_def,

                 metis empty_iff list.collapse list.set(1))

  qed

qed

lemma wq_es_cs:

  "wq (e#s) cs = wq'"

 using wq_s_cs[unfolded wq_def]

 by (auto simp:Let_def wq_def rest_def wq'_def is_v, simp) 

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

  shows "distinct (wq (e#s) cs')"

proof(cases "cs' = cs")

  case True

  show ?thesis

  proof(unfold True wq_es_cs wq'_def, rule someI2)

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

        using assms[unfolded True wq_s_cs] by auto

  qed simp

qed (insert assms, simp)

end

context valid_trace_set

begin

lemma wq_neq_simp [simp]:

  shows "wq (e#s) cs' = wq s cs'"

    using assms unfolding is_set wq_def

  by (auto simp:Let_def)

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

  shows "distinct (wq (e#s) cs')"

  using assms by simp

end

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 wq_distinct: "distinct (wq s cs)"

proof(induct rule:ind)

  case (Cons s e)

  interpret vt_e: valid_trace_e s e using Cons by simp

  show ?case 

  proof(cases e)

    case (Create th prio)

    interpret vt_create: valid_trace_create s e th prio 

      using Create by (unfold_locales, simp)

    show ?thesis using Cons by (simp add: vt_create.wq_distinct_kept) 

  next

    case (Exit th)

    interpret vt_exit: valid_trace_exit s e th  

        using Exit by (unfold_locales, simp)

    show ?thesis using Cons by (simp add: vt_exit.wq_distinct_kept) 

  next

    case (P th cs)

    interpret vt_p: valid_trace_p s e th cs using P by (unfold_locales, simp)

    show ?thesis using Cons by (simp add: vt_p.wq_distinct_kept) 

  next

    case (V th cs)

    interpret vt_v: valid_trace_v s e th cs using V by (unfold_locales, simp)

    show ?thesis using Cons by (simp add: vt_v.wq_distinct_kept) 

  next

    case (Set th prio)

    interpret vt_set: valid_trace_set s e th prio

        using Set by (unfold_locales, simp)

    show ?thesis using Cons by (simp add: vt_set.wq_distinct_kept) 

  qed

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

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

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