pip: CpsG.thy_1_1@3d2b59f15f26

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)"
  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 t1 t2 cs1 cs2
    assume  lt1: "t1 < length s"
    and np1: "\<not> ?Q cs1 (moment t1 s)"
    and nn1: "(\<forall>i'>t1. ?Q cs1 (moment i' s))"
    and lt2: "t2 < length s"
    and np2: "\<not> ?Q cs2 (moment t2 s)"
    and nn2: "(\<forall>i'>t2. ?Q cs2 (moment i' s))"
    and 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 -
      have "thread \<in> runing (moment t2 s)"
      proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
        case True
        have "e = V thread cs2"
        proof -
          have eq_th: "thread = hd (wq (moment t2 s) cs2)" 
              using True and np2  by auto 
          from vt_e.wq_out_inv[OF True this h2]
          show ?thesis .
        qed
        thus ?thesis using vt_e.actor_inv[OF vt_e.pip_e] by auto
      next
        case False
        have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
        with vt_e.actor_inv[OF vt_e.pip_e]
        show ?thesis by auto
      qed
      moreover have "thread \<notin> runing (moment t2 s)"
        by (rule q_not_runing[OF nn1[rule_format, OF lt12]])
      ultimately show ?thesis by simp
    qed
  } note lt_case = this
  show ?thesis
  proof -
    { assume "t1 < t2"
      from lt_case[OF lt1 np1 nn1 lt2 np2 nn2 this]
      have ?thesis .
    } moreover {
      assume "t2 < t1"
      from lt_case[OF lt2 np2 nn2 lt1 np1 nn1 this]
      have ?thesis .
    } moreover {
      assume eq_12: "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 lt_2: "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
      from nn1[rule_format, OF lt_2[folded eq_12]] eq_m[folded eq_12]
      have g1: "thread \<in> set (wq (e#moment t1 s) cs1)" and
           g2: "thread \<noteq> hd (wq (e#moment t1 s) cs1)" 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 "e = V thread cs2 \<or> e = P thread cs2"
      proof(cases "thread \<in> set (wq (moment t2 s) cs2)")
        case True
        have "e = V thread cs2"
        proof -
          have eq_th: "thread = hd (wq (moment t2 s) cs2)" 
              using True and np2  by auto 
          from vt_e.wq_out_inv[OF True this h2]
          show ?thesis .
        qed
        thus ?thesis by auto
      next
        case False
        have "e = P thread cs2" using vt_e.wq_in_inv[OF False h1] .
        thus ?thesis by auto
      qed
      moreover have "e = V thread cs1 \<or> e = P thread cs1"
      proof(cases "thread \<in> set (wq (moment t1 s) cs1)")
        case True
        have eq_th: "thread = hd (wq (moment t1 s) cs1)" 
              using True and np1  by auto 
        from vt_e.wq_out_inv[folded eq_12, OF True this g2]
        have "e = V thread cs1" .
        thus ?thesis by auto
      next
        case False
        have "e = P thread cs1" using vt_e.wq_in_inv[folded eq_12, OF False g1] .
        thus ?thesis by auto
      qed
      ultimately have ?thesis using neq12 by auto
    } ultimately show ?thesis using nat_neq_iff by blast 
  qed
qed

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

lemma waiting_unique:
  assumes "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

end

(* 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:
  assumes "holding (s::event list) th1 cs"
  and "holding s th2 cs"
  shows "th1 = th2"
 by (insert assms, unfold s_holding_def, 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

text {*
  The following three lemmas show that @{text "RAG"} does not change
  by the happening of @{text "Set"}, @{text "Create"} and @{text "Exit"}
  events, respectively.
*}

lemma RAG_set_unchanged: "(RAG (Set th prio # s)) = RAG s"
apply (unfold s_RAG_def s_waiting_def wq_def)
by (simp add:Let_def)

lemma RAG_create_unchanged: "(RAG (Create th prio # s)) = RAG s"
apply (unfold s_RAG_def s_waiting_def wq_def)
by (simp add:Let_def)

lemma RAG_exit_unchanged: "(RAG (Exit th # s)) = RAG s"
apply (unfold s_RAG_def s_waiting_def wq_def)
by (simp add:Let_def)


context valid_trace_v
begin

lemma distinct_rest: "distinct rest"
  by (simp add: distinct_tl rest_def wq_distinct)

lemma holding_cs_eq_th:
  assumes "holding s t cs"
  shows "t = th"
proof -
  from pip_e[unfolded is_v]
  show ?thesis
  proof(cases)
    case (thread_V)
    from held_unique[OF this(2) assms]
    show ?thesis by simp
  qed
qed

lemma distinct_wq': "distinct wq'"
  by (metis (mono_tags, lifting) distinct_rest  some_eq_ex wq'_def)
  
lemma th'_in_inv:
  assumes "th' \<in> set wq'"
  shows "th' \<in> set rest"
  using assms
  by (metis (mono_tags, lifting) distinct.simps(2) 
        rest_def some_eq_ex wq'_def wq_distinct wq_s_cs) 

lemma neq_t_th: 
  assumes "waiting (e#s) t c"
  shows "t \<noteq> th"
proof
  assume otherwise: "t = th"
  show False
  proof(cases "c = cs")
    case True
    have "t \<in> set wq'" 
     using assms[unfolded True s_waiting_def, folded wq_def, unfolded wq_es_cs]
     by simp 
    from th'_in_inv[OF this] have "t \<in> set rest" .
    with wq_s_cs[folded otherwise] wq_distinct[of cs]
    show ?thesis by simp
  next
    case False
    have "wq (e#s) c = wq s c" using False
        by (unfold is_v, simp)
    hence "waiting s t c" using assms 
        by (simp add: cs_waiting_def waiting_eq)
    hence "t \<notin> readys s" by (unfold readys_def, auto)
    hence "t \<notin> runing s" using runing_ready by auto 
    with runing_th_s[folded otherwise] show ?thesis by auto
  qed
qed

lemma waiting_esI1:
  assumes "waiting s t c"
      and "c \<noteq> cs" 
  shows "waiting (e#s) t c" 
proof -
  have "wq (e#s) c = wq s c" 
    using assms(2) is_v by auto
  with assms(1) show ?thesis 
    using cs_waiting_def waiting_eq by auto 
qed

lemma holding_esI2:
  assumes "c \<noteq> cs" 
  and "holding s t c"
  shows "holding (e#s) t c"
proof -
  from assms(1) have "wq (e#s) c = wq s c" using is_v by auto
  from assms(2)[unfolded s_holding_def, folded wq_def, 
                folded this, unfolded wq_def, folded s_holding_def]
  show ?thesis .
qed

lemma holding_esI1:
  assumes "holding s t c"
  and "t \<noteq> th"
  shows "holding (e#s) t c"
proof -
  have "c \<noteq> cs" using assms using holding_cs_eq_th by blast 
  from holding_esI2[OF this assms(1)]
  show ?thesis .
qed

end

context valid_trace_v_n
begin

lemma neq_wq': "wq' \<noteq> []" 
proof (unfold wq'_def, rule someI2)
  show "distinct rest \<and> set rest = set rest"
    by (simp add: distinct_rest) 
next
  fix x
  assume " distinct x \<and> set x = set rest" 
  thus "x \<noteq> []" using rest_nnl by auto
qed 

definition "taker = hd wq'"

definition "rest' = tl wq'"

lemma eq_wq': "wq' = taker # rest'"
  by (simp add: neq_wq' rest'_def taker_def)

lemma next_th_taker: 
  shows "next_th s th cs taker"
  using rest_nnl taker_def wq'_def wq_s_cs 
  by (auto simp:next_th_def)

lemma taker_unique: 
  assumes "next_th s th cs taker'"
  shows "taker' = taker"
proof -
  from assms
  obtain rest' where 
    h: "wq s cs = th # rest'" 
       "taker' = hd (SOME q. distinct q \<and> set q = set rest')"
          by (unfold next_th_def, auto)
  with wq_s_cs have "rest' = rest" by auto
  thus ?thesis using h(2) taker_def wq'_def by auto 
qed

lemma waiting_set_eq:
  "{(Th th', Cs cs) |th'. next_th s th cs th'} = {(Th taker, Cs cs)}"
  by (smt all_not_in_conv bot.extremum insertI1 insert_subset 
      mem_Collect_eq next_th_taker subsetI subset_antisym taker_def taker_unique)

lemma holding_set_eq:
  "{(Cs cs, Th th') |th'.  next_th s th cs th'} = {(Cs cs, Th taker)}"
  using next_th_taker taker_def waiting_set_eq 
  by fastforce
   
lemma holding_taker:
  shows "holding (e#s) taker cs"
    by (unfold s_holding_def, fold wq_def, unfold wq_es_cs, 
        auto simp:neq_wq' taker_def)

lemma waiting_esI2:
  assumes "waiting s t cs"
      and "t \<noteq> taker"
  shows "waiting (e#s) t cs" 
proof -
  have "t \<in> set wq'" 
  proof(unfold wq'_def, rule someI2)
    show "distinct rest \<and> set rest = set rest"
          by (simp add: distinct_rest)
  next
    fix x
    assume "distinct x \<and> set x = set rest"
    moreover have "t \<in> set rest"
        using assms(1) cs_waiting_def waiting_eq wq_s_cs by auto 
    ultimately show "t \<in> set x" by simp
  qed
  moreover have "t \<noteq> hd wq'"
    using assms(2) taker_def by auto 
  ultimately show ?thesis
    by (unfold s_waiting_def, fold wq_def, unfold wq_es_cs, simp)
qed

lemma waiting_esE:
  assumes "waiting (e#s) t c" 
  obtains "c \<noteq> cs" "waiting s t c"
     |    "c = cs" "t \<noteq> taker" "waiting s t cs" "t \<in> set rest'"
proof(cases "c = cs")
  case False
  hence "wq (e#s) c = wq s c" using is_v by auto
  with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto 
  from that(1)[OF False this] show ?thesis .
next
  case True
  from assms[unfolded s_waiting_def True, folded wq_def, unfolded wq_es_cs]
  have "t \<noteq> hd wq'" "t \<in> set wq'" by auto
  hence "t \<noteq> taker" by (simp add: taker_def) 
  moreover hence "t \<noteq> th" using assms neq_t_th by blast 
  moreover have "t \<in> set rest" by (simp add: `t \<in> set wq'` th'_in_inv) 
  ultimately have "waiting s t cs"
    by (metis cs_waiting_def list.distinct(2) list.sel(1) 
                list.set_sel(2) rest_def waiting_eq wq_s_cs)  
  show ?thesis using that(2)
  using True `t \<in> set wq'` `t \<noteq> taker` `waiting s t cs` eq_wq' by auto   
qed

lemma holding_esI1:
  assumes "c = cs"
  and "t = taker"
  shows "holding (e#s) t c"
  by (unfold assms, simp add: holding_taker)

lemma holding_esE:
  assumes "holding (e#s) t c" 
  obtains "c = cs" "t = taker"
      | "c \<noteq> cs" "holding s t c"
proof(cases "c = cs")
  case True
  from assms[unfolded True, unfolded s_holding_def, 
             folded wq_def, unfolded wq_es_cs]
  have "t = taker" by (simp add: taker_def) 
  from that(1)[OF True this] show ?thesis .
next
  case False
  hence "wq (e#s) c = wq s c" using is_v by auto
  from assms[unfolded s_holding_def, folded wq_def, 
             unfolded this, unfolded wq_def, folded s_holding_def]
  have "holding s t c"  .
  from that(2)[OF False this] show ?thesis .
qed

end 


context valid_trace_v_e
begin

lemma nil_wq': "wq' = []" 
proof (unfold wq'_def, rule someI2)
  show "distinct rest \<and> set rest = set rest"
    by (simp add: distinct_rest) 
next
  fix x
  assume " distinct x \<and> set x = set rest" 
  thus "x = []" using rest_nil by auto
qed 

lemma no_taker: 
  assumes "next_th s th cs taker"
  shows "False"
proof -
  from assms[unfolded next_th_def]
  obtain rest' where "wq s cs = th # rest'" "rest' \<noteq> []"
    by auto
  thus ?thesis using rest_def rest_nil by auto 
qed

lemma waiting_set_eq:
  "{(Th th', Cs cs) |th'. next_th s th cs th'} = {}"
  using no_taker by auto

lemma holding_set_eq:
  "{(Cs cs, Th th') |th'.  next_th s th cs th'} = {}"
  using no_taker by auto
   
lemma no_holding:
  assumes "holding (e#s) taker cs"
  shows False
proof -
  from wq_es_cs[unfolded nil_wq']
  have " wq (e # s) cs = []" .
  from assms[unfolded s_holding_def, folded wq_def, unfolded this]
  show ?thesis by auto
qed

lemma no_waiting:
  assumes "waiting (e#s) t cs"
  shows False
proof -
  from wq_es_cs[unfolded nil_wq']
  have " wq (e # s) cs = []" .
  from assms[unfolded s_waiting_def, folded wq_def, unfolded this]
  show ?thesis by auto
qed

lemma waiting_esI2:
  assumes "waiting s t c"
  shows "waiting (e#s) t c"
proof -
  have "c \<noteq> cs" using assms
    using cs_waiting_def rest_nil waiting_eq wq_s_cs by auto 
  from waiting_esI1[OF assms this]
  show ?thesis .
qed

lemma waiting_esE:
  assumes "waiting (e#s) t c" 
  obtains "c \<noteq> cs" "waiting s t c"
proof(cases "c = cs")
  case False
  hence "wq (e#s) c = wq s c" using is_v by auto
  with assms have "waiting s t c" using cs_waiting_def waiting_eq by auto 
  from that(1)[OF False this] show ?thesis .
next
  case True
  from no_waiting[OF assms[unfolded True]]
  show ?thesis by auto
qed

lemma holding_esE:
  assumes "holding (e#s) t c" 
  obtains "c \<noteq> cs" "holding s t c"
proof(cases "c = cs")
  case True
  from no_holding[OF assms[unfolded True]] 
  show ?thesis by auto
next
  case False
  hence "wq (e#s) c = wq s c" using is_v by auto
  from assms[unfolded s_holding_def, folded wq_def, 
             unfolded this, unfolded wq_def, folded s_holding_def]
  have "holding s t c"  .
  from that[OF False this] show ?thesis .
qed

end 

lemma rel_eqI:
  assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"
  and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"
  shows "A = B"
  using assms by auto

lemma in_RAG_E:
  assumes "(n1, n2) \<in> RAG (s::state)"
  obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
      | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
  using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
  by auto
  
context valid_trace_v
begin

lemma RAG_es:
  "RAG (e # s) =
   RAG s - {(Cs cs, Th th)} -
     {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
     {(Cs cs, Th th') |th'.  next_th s th cs th'}" (is "?L = ?R")
proof(rule rel_eqI)
  fix n1 n2
  assume "(n1, n2) \<in> ?L"
  thus "(n1, n2) \<in> ?R"
  proof(cases rule:in_RAG_E)
    case (waiting th' cs')
    show ?thesis
    proof(cases "rest = []")
      case False
      interpret h_n: valid_trace_v_n s e th cs
        by (unfold_locales, insert False, simp)
      from waiting(3)
      show ?thesis
      proof(cases rule:h_n.waiting_esE)
        case 1
        with waiting(1,2)
        show ?thesis
        by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 
             fold waiting_eq, auto)
      next
        case 2
        with waiting(1,2)
        show ?thesis
         by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 
             fold waiting_eq, auto)
      qed
    next
      case True
      interpret h_e: valid_trace_v_e s e th cs
        by (unfold_locales, insert True, simp)
      from waiting(3)
      show ?thesis
      proof(cases rule:h_e.waiting_esE)
        case 1
        with waiting(1,2)
        show ?thesis
        by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, 
             fold waiting_eq, auto)
      qed
    qed
  next
    case (holding th' cs')
    show ?thesis
    proof(cases "rest = []")
      case False
      interpret h_n: valid_trace_v_n s e th cs
        by (unfold_locales, insert False, simp)
      from holding(3)
      show ?thesis
      proof(cases rule:h_n.holding_esE)
        case 1
        with holding(1,2)
        show ?thesis
        by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 
             fold waiting_eq, auto)
      next
        case 2
        with holding(1,2)
        show ?thesis
         by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def, 
             fold holding_eq, auto)
      qed
    next
      case True
      interpret h_e: valid_trace_v_e s e th cs
        by (unfold_locales, insert True, simp)
      from holding(3)
      show ?thesis
      proof(cases rule:h_e.holding_esE)
        case 1
        with holding(1,2)
        show ?thesis
        by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def, 
             fold holding_eq, auto)
      qed
    qed
  qed
next
  fix n1 n2
  assume h: "(n1, n2) \<in> ?R"
  show "(n1, n2) \<in> ?L"
  proof(cases "rest = []")
    case False
    interpret h_n: valid_trace_v_n s e th cs
        by (unfold_locales, insert False, simp)
    from h[unfolded h_n.waiting_set_eq h_n.holding_set_eq]
    have "((n1, n2) \<in> RAG s \<and> (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th)
                            \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)) \<or> 
          (n2 = Th h_n.taker \<and> n1 = Cs cs)" 
      by auto
   thus ?thesis
   proof
      assume "n2 = Th h_n.taker \<and> n1 = Cs cs"
      with h_n.holding_taker
      show ?thesis 
        by (unfold s_RAG_def, fold holding_eq, auto)
   next
    assume h: "(n1, n2) \<in> RAG s \<and>
        (n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)"
    hence "(n1, n2) \<in> RAG s" by simp
    thus ?thesis
    proof(cases rule:in_RAG_E)
      case (waiting th' cs')
      from h and this(1,2)
      have "th' \<noteq> h_n.taker \<or> cs' \<noteq> cs" by auto
      hence "waiting (e#s) th' cs'" 
      proof
        assume "cs' \<noteq> cs"
        from waiting_esI1[OF waiting(3) this] 
        show ?thesis .
      next
        assume neq_th': "th' \<noteq> h_n.taker"
        show ?thesis
        proof(cases "cs' = cs")
          case False
          from waiting_esI1[OF waiting(3) this] 
          show ?thesis .
        next
          case True
          from h_n.waiting_esI2[OF waiting(3)[unfolded True] neq_th', folded True]
          show ?thesis .
        qed
      qed
      thus ?thesis using waiting(1,2)
        by (unfold s_RAG_def, fold waiting_eq, auto)
    next
      case (holding th' cs')
      from h this(1,2)
      have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto
      hence "holding (e#s) th' cs'"
      proof
        assume "cs' \<noteq> cs"
        from holding_esI2[OF this holding(3)] 
        show ?thesis .
      next
        assume "th' \<noteq> th"
        from holding_esI1[OF holding(3) this]
        show ?thesis .
      qed
      thus ?thesis using holding(1,2)
        by (unfold s_RAG_def, fold holding_eq, auto)
    qed
   qed
 next
   case True
   interpret h_e: valid_trace_v_e s e th cs
        by (unfold_locales, insert True, simp)
   from h[unfolded h_e.waiting_set_eq h_e.holding_set_eq]
   have h_s: "(n1, n2) \<in> RAG s" "(n1, n2) \<noteq> (Cs cs, Th th)" 
      by auto
   from h_s(1)
   show ?thesis
   proof(cases rule:in_RAG_E)
    case (waiting th' cs')
    from h_e.waiting_esI2[OF this(3)]
    show ?thesis using waiting(1,2)
      by (unfold s_RAG_def, fold waiting_eq, auto)
   next
    case (holding th' cs')
    with h_s(2)
    have "cs' \<noteq> cs \<or> th' \<noteq> th" by auto
    thus ?thesis
    proof
      assume neq_cs: "cs' \<noteq> cs"
      from holding_esI2[OF this holding(3)]
      show ?thesis using holding(1,2)
        by (unfold s_RAG_def, fold holding_eq, auto)
    next
      assume "th' \<noteq> th"
      from holding_esI1[OF holding(3) this]
      show ?thesis using holding(1,2)
        by (unfold s_RAG_def, fold holding_eq, auto)
    qed
   qed
 qed
qed

end

lemma step_RAG_v: 
assumes vt:
  "vt (V th cs#s)"
shows "
  RAG (V th cs # s) =
  RAG s - {(Cs cs, Th th)} -
  {(Th th', Cs cs) |th'. next_th s th cs th'} \<union>
  {(Cs cs, Th th') |th'.  next_th s th cs th'}" (is "?L = ?R")
proof -
  interpret vt_v: valid_trace_v s "V th cs"
    using assms step_back_vt by (unfold_locales, auto) 
  show ?thesis using vt_v.RAG_es .
qed

lemma (in valid_trace_create)
  th_not_in_threads: "th \<notin> threads s"
proof -
  from pip_e[unfolded is_create]
  show ?thesis by (cases, simp)
qed

lemma (in valid_trace_create)
  threads_es [simp]: "threads (e#s) = threads s \<union> {th}"
  by (unfold is_create, simp)

lemma (in valid_trace_exit)
  threads_es [simp]: "threads (e#s) = threads s - {th}"
  by (unfold is_exit, simp)

lemma (in valid_trace_p)
  threads_es [simp]: "threads (e#s) = threads s"
  by (unfold is_p, simp)

lemma (in valid_trace_v)
  threads_es [simp]: "threads (e#s) = threads s"
  by (unfold is_v, simp)

lemma (in valid_trace_v)
  th_not_in_rest[simp]: "th \<notin> set rest"
proof
  assume otherwise: "th \<in> set rest"
  have "distinct (wq s cs)" by (simp add: wq_distinct)
  from this[unfolded wq_s_cs] and otherwise
  show False by auto
qed

lemma (in valid_trace_v)
  set_wq_es_cs [simp]: "set (wq (e#s) cs) = set (wq s cs) - {th}"
proof(unfold wq_es_cs wq'_def, rule someI2)
  show "distinct rest \<and> set rest = set rest"
    by (simp add: distinct_rest)
next
  fix x
  assume "distinct x \<and> set x = set rest"
  thus "set x = set (wq s cs) - {th}" 
      by (unfold wq_s_cs, simp)
qed

lemma (in valid_trace_exit)
  th_not_in_wq: "th \<notin> set (wq s cs)"
proof -
  from pip_e[unfolded is_exit]
  show ?thesis
  by (cases, unfold holdents_def s_holding_def, fold wq_def, 
             auto elim!:runing_wqE)
qed

lemma (in valid_trace) wq_threads: 
  assumes "th \<in> set (wq s cs)"
  shows "th \<in> threads s"
  using assms
proof(induct rule:ind)
  case (Nil)
  thus ?case by (auto simp:wq_def)
next
  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: valid_trace_create s e th' prio'
      using Create by (unfold_locales, simp)
    show ?thesis
      using Cons.hyps(2) Cons.prems by auto
  next
    case (Exit th')
    interpret vt: valid_trace_exit s e th'
      using Exit by (unfold_locales, simp)
    show ?thesis
      using Cons.hyps(2) Cons.prems vt.th_not_in_wq by auto 
  next
    case (P th' cs')
    interpret vt: valid_trace_p s e th' cs'
      using P by (unfold_locales, simp)
    show ?thesis
      using Cons.hyps(2) Cons.prems readys_threads 
        runing_ready vt.is_p vt.runing_th_s vt_e.wq_in_inv 
        by fastforce 
  next
    case (V th' cs')
    interpret vt: valid_trace_v s e th' cs'
      using V by (unfold_locales, simp)
    show ?thesis using Cons
      using vt.is_v vt.threads_es vt_e.wq_in_inv by blast
  next
    case (Set th' prio)
    interpret vt: valid_trace_set s e th' prio
      using Set by (unfold_locales, simp)
    show ?thesis using Cons.hyps(2) Cons.prems vt.is_set 
        by (auto simp:wq_def Let_def)
  qed
qed 

context valid_trace
begin

lemma  dm_RAG_threads:
  assumes in_dom: "(Th th) \<in> Domain (RAG s)"
  shows "th \<in> threads s"
proof -
  from in_dom obtain n where "(Th th, n) \<in> RAG s" by auto
  moreover from RAG_target_th[OF this] obtain cs where "n = Cs cs" by auto
  ultimately have "(Th th, Cs cs) \<in> RAG s" by simp
  hence "th \<in> set (wq s cs)"
    by (unfold s_RAG_def, auto simp:cs_waiting_def)
  from wq_threads [OF this] show ?thesis .
qed

lemma  cp_le:
  assumes th_in: "th \<in> threads s"
  shows "cp s th \<le> Max ((\<lambda> th. (preced th s)) ` threads s)"
proof(unfold cp_eq_cpreced cpreced_def cs_dependants_def)
  show "Max ((\<lambda>th. preced th s) ` ({th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+}))
         \<le> Max ((\<lambda>th. preced th s) ` threads s)"
    (is "Max (?f ` ?A) \<le> Max (?f ` ?B)")
  proof(rule Max_f_mono)
    show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<noteq> {}" by simp
  next
    from finite_threads
    show "finite (threads s)" .
  next
    from th_in
    show "{th} \<union> {th'. (Th th', Th th) \<in> (RAG (wq s))\<^sup>+} \<subseteq> threads s"
      apply (auto simp:Domain_def)
      apply (rule_tac dm_RAG_threads)
      apply (unfold trancl_domain [of "RAG s", symmetric])
      by (unfold cs_RAG_def s_RAG_def, auto simp:Domain_def)
  qed
qed

lemma max_cp_eq: 
  shows "Max ((cp s) ` threads s) = Max ((\<lambda> th. (preced th s)) ` threads s)"
  (is "?l = ?r")
proof(cases "threads s = {}")
  case True
  thus ?thesis by auto
next
  case False
  have "?l \<in> ((cp s) ` threads s)"
  proof(rule Max_in)
    from finite_threads
    show "finite (cp s ` threads s)" by auto
  next
    from False show "cp s ` threads s \<noteq> {}" by auto
  qed
  then obtain th 
    where th_in: "th \<in> threads s" and eq_l: "?l = cp s th" by auto
  have "\<dots> \<le> ?r" by (rule cp_le[OF th_in])
  moreover have "?r \<le> cp s th" (is "Max (?f ` ?A) \<le> cp s th")
  proof -
    have "?r \<in> (?f ` ?A)"
    proof(rule Max_in)
      from finite_threads
      show " finite ((\<lambda>th. preced th s) ` threads s)" by auto
    next
      from False show " (\<lambda>th. preced th s) ` threads s \<noteq> {}" by auto
    qed
    then obtain th' where 
      th_in': "th' \<in> ?A " and eq_r: "?r = ?f th'" by auto
    from le_cp [of th']  eq_r
    have "?r \<le> cp s th'" 
    moreover have "\<dots> \<le> cp s th"
    proof(fold eq_l)
      show " cp s th' \<le> Max (cp s ` threads s)"
      proof(rule Max_ge)
        from th_in' show "cp s th' \<in> cp s ` threads s"
          by auto
      next
        from finite_threads
        show "finite (cp s ` threads s)" by auto
      qed
    qed
    ultimately show ?thesis by auto
  qed
  ultimately show ?thesis using eq_l by auto
qed

lemma max_cp_eq_the_preced:
  shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
  using max_cp_eq using the_preced_def by presburger 

end

lemma preced_v [simp]: "preced th' (V th cs#s) = preced th' s"
  by (unfold preced_def, simp)

lemma (in valid_trace_v)
  preced_es: "preced th (e#s) = preced th s"
  by (unfold is_v preced_def, simp)

lemma the_preced_v[simp]: "the_preced (V th cs#s) = the_preced s"
proof
  fix th'
  show "the_preced (V th cs # s) th' = the_preced s th'"
    by (unfold the_preced_def preced_def, simp)
qed

lemma (in valid_trace_v)
  the_preced_es: "the_preced (e#s) = the_preced s"
  by (unfold is_v preced_def, simp)

context valid_trace_p
begin

lemma not_holding_es_th_cs: "\<not> holding s th cs"
proof
  assume otherwise: "holding s th cs"
  from pip_e[unfolded is_p]
  show False
  proof(cases)
    case (thread_P)
    moreover have "(Cs cs, Th th) \<in> RAG s"
      using otherwise cs_holding_def 
            holding_eq th_not_in_wq by auto
    ultimately show ?thesis by auto
  qed
qed

lemma waiting_kept:
  assumes "waiting s th' cs'"
  shows "waiting (e#s) th' cs'"
  using assms
  by (metis cs_waiting_def hd_append2 list.sel(1) list.set_intros(2) 
      rotate1.simps(2) self_append_conv2 set_rotate1 
        th_not_in_wq waiting_eq wq_es_cs wq_neq_simp)
  
lemma holding_kept:
  assumes "holding s th' cs'"
  shows "holding (e#s) th' cs'"
proof(cases "cs' = cs")
  case False
  hence "wq (e#s) cs' = wq s cs'" by simp
  with assms show ?thesis using cs_holding_def holding_eq by auto 
next
  case True
  from assms[unfolded s_holding_def, folded wq_def]
  obtain rest where eq_wq: "wq s cs' = th'#rest"
    by (metis empty_iff list.collapse list.set(1)) 
  hence "wq (e#s) cs' = th'#(rest@[th])"
    by (simp add: True wq_es_cs) 
  thus ?thesis
    by (simp add: cs_holding_def holding_eq) 
qed

end

locale valid_trace_p_h = valid_trace_p +
  assumes we: "wq s cs = []"

locale valid_trace_p_w = valid_trace_p +
  assumes wne: "wq s cs \<noteq> []"
begin

definition "holder = hd (wq s cs)"
definition "waiters = tl (wq s cs)"
definition "waiters' = waiters @ [th]"

lemma wq_s_cs: "wq s cs = holder#waiters"
    by (simp add: holder_def waiters_def wne)
    
lemma wq_es_cs': "wq (e#s) cs = holder#waiters@[th]"
  by (simp add: wq_es_cs wq_s_cs)

lemma waiting_es_th_cs: "waiting (e#s) th cs"
  using cs_waiting_def th_not_in_wq waiting_eq wq_es_cs' wq_s_cs by auto

lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"
   by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto)

lemma holding_esE:
  assumes "holding (e#s) th' cs'"
  obtains "holding s th' cs'"
  using assms 
proof(cases "cs' = cs")
  case False
  hence "wq (e#s) cs' = wq s cs'" by simp
  with assms show ?thesis
    using cs_holding_def holding_eq that by auto 
next
  case True
  with assms show ?thesis
  by (metis cs_holding_def holding_eq list.sel(1) list.set_intros(1) that 
        wq_es_cs' wq_s_cs) 
qed

lemma waiting_esE:
  assumes "waiting (e#s) th' cs'"
  obtains "th' \<noteq> th" "waiting s th' cs'"
     |  "th' = th" "cs' = cs"
proof(cases "waiting s th' cs'")
  case True
  have "th' \<noteq> th"
  proof
    assume otherwise: "th' = th"
    from True[unfolded this]
    show False by (simp add: th_not_waiting) 
  qed
  from that(1)[OF this True] show ?thesis .
next
  case False
  hence "th' = th \<and> cs' = cs"
      by (metis assms cs_waiting_def holder_def list.sel(1) rotate1.simps(2) 
        set_ConsD set_rotate1 waiting_eq wq_es_cs wq_es_cs' wq_neq_simp)
  with that(2) show ?thesis by metis
qed

lemma RAG_es: "RAG (e # s) =  RAG s \<union> {(Th th, Cs cs)}" (is "?L = ?R")
proof(rule rel_eqI)
  fix n1 n2
  assume "(n1, n2) \<in> ?L"
  thus "(n1, n2) \<in> ?R" 
  proof(cases rule:in_RAG_E)
    case (waiting th' cs')
    from this(3)
    show ?thesis
    proof(cases rule:waiting_esE)
      case 1
      thus ?thesis using waiting(1,2)
        by (unfold s_RAG_def, fold waiting_eq, auto)
    next
      case 2
      thus ?thesis using waiting(1,2) by auto
    qed
  next
    case (holding th' cs')
    from this(3)
    show ?thesis
    proof(cases rule:holding_esE)
      case 1
      with holding(1,2)
      show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
    qed
  qed
next
  fix n1 n2
  assume "(n1, n2) \<in> ?R"
  hence "(n1, n2) \<in> RAG s \<or> (n1 = Th th \<and> n2 = Cs cs)" by auto
  thus "(n1, n2) \<in> ?L"
  proof
    assume "(n1, n2) \<in> RAG s"
    thus ?thesis
    proof(cases rule:in_RAG_E)
      case (waiting th' cs')
      from waiting_kept[OF this(3)]
      show ?thesis using waiting(1,2)
         by (unfold s_RAG_def, fold waiting_eq, auto)
    next
      case (holding th' cs')
      from holding_kept[OF this(3)]
      show ?thesis using holding(1,2)
         by (unfold s_RAG_def, fold holding_eq, auto)
    qed
  next
    assume "n1 = Th th \<and> n2 = Cs cs"
    thus ?thesis using RAG_edge by auto
  qed
qed

end

context valid_trace_p_h
begin

lemma wq_es_cs': "wq (e#s) cs = [th]"
  using wq_es_cs[unfolded we] by simp

lemma holding_es_th_cs: 
  shows "holding (e#s) th cs"
proof -
  from wq_es_cs'
  have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto
  thus ?thesis using cs_holding_def holding_eq by blast 
qed

lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)"
  by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto)

lemma waiting_esE:
  assumes "waiting (e#s) th' cs'"
  obtains "waiting s th' cs'"
  using assms
  by (metis cs_waiting_def event.distinct(15) is_p list.sel(1) 
        set_ConsD waiting_eq we wq_es_cs' wq_neq_simp wq_out_inv)
  
lemma holding_esE:
  assumes "holding (e#s) th' cs'"
  obtains "cs' \<noteq> cs" "holding s th' cs'"
    | "cs' = cs" "th' = th"
proof(cases "cs' = cs")
  case True
  from held_unique[OF holding_es_th_cs assms[unfolded True]]
  have "th' = th" by simp
  from that(2)[OF True this] show ?thesis .
next
  case False
  have "holding s th' cs'" using assms
    using False cs_holding_def holding_eq by auto
  from that(1)[OF False this] show ?thesis .
qed

lemma RAG_es: "RAG (e # s) =  RAG s \<union> {(Cs cs, Th th)}" (is "?L = ?R")
proof(rule rel_eqI)
  fix n1 n2
  assume "(n1, n2) \<in> ?L"
  thus "(n1, n2) \<in> ?R" 
  proof(cases rule:in_RAG_E)
    case (waiting th' cs')
    from this(3)
    show ?thesis
    proof(cases rule:waiting_esE)
      case 1
      thus ?thesis using waiting(1,2)
        by (unfold s_RAG_def, fold waiting_eq, auto)
    qed
  next
    case (holding th' cs')
    from this(3)
    show ?thesis
    proof(cases rule:holding_esE)
      case 1
      with holding(1,2)
      show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
    next
      case 2
      with holding(1,2) show ?thesis by auto
    qed
  qed
next
  fix n1 n2
  assume "(n1, n2) \<in> ?R"
  hence "(n1, n2) \<in> RAG s \<or> (n1 = Cs cs \<and> n2 = Th th)" by auto
  thus "(n1, n2) \<in> ?L"
  proof
    assume "(n1, n2) \<in> RAG s"
    thus ?thesis
    proof(cases rule:in_RAG_E)
      case (waiting th' cs')
      from waiting_kept[OF this(3)]
      show ?thesis using waiting(1,2)
         by (unfold s_RAG_def, fold waiting_eq, auto)
    next
      case (holding th' cs')
      from holding_kept[OF this(3)]
      show ?thesis using holding(1,2)
         by (unfold s_RAG_def, fold holding_eq, auto)
    qed
  next
    assume "n1 = Cs cs \<and> n2 = Th th"
    with holding_es_th_cs
    show ?thesis 
      by (unfold s_RAG_def, fold holding_eq, auto)
  qed
qed

end

context valid_trace_p
begin

lemma RAG_es': "RAG (e # s) =  (if (wq s cs = []) then RAG s \<union> {(Cs cs, Th th)}
                                                  else RAG s \<union> {(Th th, Cs cs)})"
proof(cases "wq s cs = []")
  case True
  interpret vt_p: valid_trace_p_h using True
    by (unfold_locales, simp)
  show ?thesis by (simp add: vt_p.RAG_es vt_p.we) 
next
  case False
  interpret vt_p: valid_trace_p_w using False
    by (unfold_locales, simp)
  show ?thesis by (simp add: vt_p.RAG_es vt_p.wne) 
qed

end


end
author	zhangx
	Mon, 01 Feb 2016 20:56:39 +0800 (2016-02-01)
changeset 100	3d2b59f15f26
parent 81	c495eb16beb6
permissions	-rw-r--r--