theory CpsG

imports PIPDefs

begin

lemma Max_fg_mono:

  assumes "finite A"

  and "\<forall> a \<in> A. f a \<le> g a"

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

proof(cases "A = {}")

  case True

  thus ?thesis by auto

next

  case False

  show ?thesis

  proof(rule Max.boundedI)

    from assms show "finite (f ` A)" by auto

  next

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

  next

    fix fa

    assume "fa \<in> f ` A"

    then obtain a where h_fa: "a \<in> A" "fa = f a" by auto

    show "fa \<le> Max (g ` A)"

    proof(rule Max_ge_iff[THEN iffD2])

      from assms show "finite (g ` A)" by auto

    next

      from False show "g ` A \<noteq> {}" by auto

    next

      from h_fa have "g a \<in> g ` A" by auto

      moreover have "fa \<le> g a" using h_fa assms(2) by auto

      ultimately show "\<exists>a\<in>g ` A. fa \<le> a" by auto

    qed

  qed

qed 

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

lemma eq_RAG: 

  "RAG (wq s) = RAG s"

  by (unfold cs_RAG_def s_RAG_def, auto)

lemma waiting_holding:

  assumes "waiting (s::state) th cs"

  obtains th' where "holding s th' cs"

proof -

  from assms[unfolded s_waiting_def, folded wq_def]

  obtain th' where "th' \<in> set (wq s cs)" "th' = hd (wq s cs)"

    by (metis empty_iff hd_in_set list.set(1))

  hence "holding s th' cs" 

    by (unfold s_holding_def, fold wq_def, auto)

  from that[OF this] show ?thesis .

qed

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

  "cp s th =  

           Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"

proof -

  have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =

        Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 

          (is "Max (_ ` ?L) = Max (_ ` ?R)")

  proof -

    have "?L = ?R" 

    by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)

    thus ?thesis by simp

  qed

  thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)

qed

(* ccc *)

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 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 ready_th_s: "th \<in> readys s"

  using runing_th_s

  by (unfold runing_def, auto)

lemma live_th_s: "th \<in> threads s"

  using readys_threads ready_th_s by auto

lemma live_th_es: "th \<in> threads (e#s)"

  using live_th_s 

  by (unfold is_p, simp)

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