pip: PIPBasics.thy@c7db2ccba18a

theory PIPBasics
imports PIPDefs
begin

section {* Generic aulxiliary lemmas *}

lemma f_image_eq:
  assumes h: "\<And> a. a \<in> A \<Longrightarrow> f a = g a"
  shows "f ` A = g ` A"
proof
  show "f ` A \<subseteq> g ` A"
    by(rule image_subsetI, auto intro:h)
next
  show "g ` A \<subseteq> f ` A"
   by (rule image_subsetI, auto intro:h[symmetric])
qed

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 Max_UNION: 
  assumes "finite A"
  and "A \<noteq> {}"
  and "\<forall> M \<in> f ` A. finite M"
  and "\<forall> M \<in> f ` A. M \<noteq> {}"
  shows "Max (\<Union>x\<in> A. f x) = Max (Max ` f ` A)" (is "?L = ?R")
  using assms[simp]
proof -
  have "?L = Max (\<Union>(f ` A))"
    by (fold Union_image_eq, simp)
  also have "... = ?R"
    by (subst Max_Union, simp+)
  finally show ?thesis .
qed

lemma max_Max_eq:
  assumes "finite A"
    and "A \<noteq> {}"
    and "x = y"
  shows "max x (Max A) = Max ({y} \<union> A)" (is "?L = ?R")
proof -
  have "?R = Max (insert y A)" by simp
  also from assms have "... = ?L"
      by (subst Max.insert, simp+)
  finally show ?thesis by simp
qed

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

section {* Lemmas do not depend on trace validity *}

lemma birth_time_lt:  
  assumes "s \<noteq> []"
  shows "last_set th s < length s"
  using assms
proof(induct s)
  case (Cons a s)
  show ?case
  proof(cases "s \<noteq> []")
    case False
    thus ?thesis
      by (cases a, auto)
  next
    case True
    show ?thesis using Cons(1)[OF True]
      by (cases a, auto)
  qed
qed simp

lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"
  by (induct s, auto)

lemma preced_tm_lt: "th \<in> threads s \<Longrightarrow> preced th s = Prc x y \<Longrightarrow> y < length s"
  by (drule_tac th_in_ne, unfold preced_def, auto intro: birth_time_lt)

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

lemma RAG_target_th: "(Th th, x) \<in> RAG (s::state) \<Longrightarrow> \<exists> cs. x = Cs cs"
  by (unfold s_RAG_def, 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 children_RAG_alt_def:
  "children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"
  by (unfold s_RAG_def, auto simp:children_def holding_eq)

lemma holdents_alt_def:
  "holdents s th = the_cs ` (children (RAG (s::state)) (Th th))"
  by (unfold children_RAG_alt_def holdents_def, simp add: image_image)

lemma cntCS_alt_def:
  "cntCS s th = card (children (RAG s) (Th th))"
  apply (unfold children_RAG_alt_def cntCS_def holdents_def)
  by (rule card_image[symmetric], auto simp:inj_on_def)

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)

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

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) 


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

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

lemma count_rec1 [simp]: 
  assumes "Q e"
  shows "count Q (e#es) = Suc (count Q es)"
  using assms
  by (unfold count_def, auto)

lemma count_rec2 [simp]: 
  assumes "\<not>Q e"
  shows "count Q (e#es) = (count Q es)"
  using assms
  by (unfold count_def, auto)

lemma count_rec3 [simp]: 
  shows "count Q [] =  0"
  by (unfold count_def, auto)

lemma cntP_simp1[simp]:
  "cntP (P th cs'#s) th = cntP s th + 1"
  by (unfold cntP_def, simp)

lemma cntP_simp2[simp]:
  assumes "th' \<noteq> th"
  shows "cntP (P th cs'#s) th' = cntP s th'"
  using assms
  by (unfold cntP_def, simp)

lemma cntP_simp3[simp]:
  assumes "\<not> isP e"
  shows "cntP (e#s) th' = cntP s th'"
  using assms
  by (unfold cntP_def, cases e, simp+)

lemma cntV_simp1[simp]:
  "cntV (V th cs'#s) th = cntV s th + 1"
  by (unfold cntV_def, simp)

lemma cntV_simp2[simp]:
  assumes "th' \<noteq> th"
  shows "cntV (V th cs'#s) th' = cntV s th'"
  using assms
  by (unfold cntV_def, simp)

lemma cntV_simp3[simp]:
  assumes "\<not> isV e"
  shows "cntV (e#s) th' = cntV s th'"
  using assms
  by (unfold cntV_def, cases e, simp+)

lemma cntP_diff_inv:
  assumes "cntP (e#s) th \<noteq> cntP s th"
  shows "isP e \<and> actor e = th"
proof(cases e)
  case (P th' pty)
  show ?thesis
  by (cases "(\<lambda>e. \<exists>cs. e = P th cs) (P th' pty)", 
        insert assms P, auto simp:cntP_def)
qed (insert assms, auto simp:cntP_def)
  
lemma cntV_diff_inv:
  assumes "cntV (e#s) th \<noteq> cntV s th"
  shows "isV e \<and> actor e = th"
proof(cases e)
  case (V th' pty)
  show ?thesis
  by (cases "(\<lambda>e. \<exists>cs. e = V th cs) (V th' pty)", 
        insert assms V, auto simp:cntV_def)
qed (insert assms, auto simp:cntV_def)

lemma eq_dependants: "dependants (wq s) = dependants s"
  by (simp add: s_dependants_abv wq_def)

lemma inj_the_preced: 
  "inj_on (the_preced s) (threads s)"
  by (metis inj_onI preced_unique the_preced_def)

(* ccc *)

section {* Locales used to investigate the execution of PIP *}

text {* 
  The following locale @{text valid_trace} is used to constrain the 
  trace to be valid. All properties hold for valid traces are 
  derived under this locale. 
*}
locale valid_trace = 
  fixes s
  assumes vt : "vt s"

text {* 
  The following locale @{text valid_trace_e} describes 
  the valid extension of a valid trace. The event @{text "e"}
  represents an event in the system, which corresponds 
  to a one step operation of the PIP protocol. 
  It is required that @{text "e"} is an event eligible to happen
  under state @{text "s"}, which is already required to be valid
  by the parent locale @{text "valid_trace"}.

  This locale is used to investigate one step execution of PIP, 
  properties concerning the effects of @{text "e"}'s execution, 
  for example, how the values of observation functions are changed, 
  or how desirable properties are kept invariant, are derived
  under this locale. The state before execution is @{text "s"}, while
  the state after execution is @{text "e#s"}. Therefore, the lemmas 
  derived usually relate observations on @{text "e#s"} to those 
  on @{text "s"}.
*}

locale valid_trace_e = valid_trace +
  fixes e
  assumes vt_e: "vt (e#s)"
begin

text {*
  The following lemma shows that @{text "e"} must be a 
  eligible event (or a valid step) to be taken under
  the state represented by @{text "s"}.
*}
lemma pip_e: "PIP s e"
  using vt_e by (cases, simp)  

end

text {*
  Because @{term "e#s"} is also a valid trace, properties 
  derived for valid trace @{term s} also hold on @{term "e#s"}.
*}
sublocale valid_trace_e < vat_es!: valid_trace "e#s" 
  using vt_e
  by (unfold_locales, simp)

text {*
  For each specific event (or operation), there is a sublocale
  further constraining that the event @{text e} to be that 
  particular event. 

  For example, the following 
  locale @{text "valid_trace_create"} is the sublocale for 
  event @{term "Create"}:
*}
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"

text {*
  locale @{text "valid_trace_p"} is divided further into two 
  sublocales, namely, @{text "valid_trace_p_h"} 
  and @{text "valid_trace_p_w"}.
*}

text {*
  The following two sublocales @{text "valid_trace_p_h"}
  and @{text "valid_trace_p_w"} represent two complementary 
  cases under @{text "valid_trace_p"}, where
  @{text "valid_trace_p_h"} further constraints that
  @{text "wq s cs = []"}, which means the waiting queue of 
  the requested resource @{text "cs"} is empty, in which
  case,  the requesting thread @{text "th"} 
  will take hold of @{text "cs"}. 

  Opposite to @{text "valid_trace_p_h"},
  @{text "valid_trace_p_w"} constraints that
  @{text "wq s cs \<noteq> []"}, which means the waiting queue of 
  the requested resource @{text "cs"} is nonempty, in which
  case,  the requesting thread @{text "th"} will be blocked
  on @{text "cs"}: 

  Peculiar properties will be derived under respective 
  locales.
*}

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

text {*
  The following @{text "holder"} designates
  the holder of @{text "cs"} before the @{text "P"}-operation.
*}
definition "holder = hd (wq s cs)"

text {*
  The following @{text "waiters"} designates
  the list of threads waiting for @{text "cs"} 
  before the @{text "P"}-operation.
*}
definition "waiters = tl (wq s cs)"
end

text {* 
  @{text "valid_trace_v"} is set for the @{term V}-operation.
*}
locale valid_trace_v = valid_trace_e + 
  fixes th cs
  assumes is_v: "e = V th cs"
begin
  -- {* The following @{text "rest"} is the tail of 
        waiting queue of the resource @{text "cs"}
        to be released by this @{text "V"}-operation.
     *}
  definition "rest = tl (wq s cs)"

  text {*
    The following @{text "wq'"} is the waiting
    queue of @{term "cs"}
    after the @{text "V"}-operation, which
    is simply a reordering of @{term "rest"}. 

    The effect of this reordering needs to be 
    understood by two cases:
    \begin{enumerate}
    \item When @{text "rest = []"},
    the reordering gives rise to an empty list as well, 
    which means there is no thread holding or waiting 
    for resource @{term "cs"}, therefore, it is free.

    \item When @{text "rest \<noteq> []"}, the effect of 
    this reordering is to arbitrarily 
    switch one thread in @{term "rest"} to the 
    head, which, by definition take over the hold
    of @{term "cs"} and is designated by @{text "taker"}
    in the following sublocale @{text "valid_trace_v_n"}.
  *}
  definition "wq' = (SOME q. distinct q \<and> set q = set rest)"

  text {* 
  The following @{text "rest'"} is the tail of the 
  waiting queue after the @{text "V"}-operation. 
  It plays only auxiliary role to ease reasoning. 
  *}
  definition "rest' = tl wq'"

end

text {* 
  In the following, @{text "valid_trace_v"} is also 
  divided into two 
  sublocales: when @{text "rest"} is empty (represented
  by @{text "valid_trace_v_e"}), which means, there is no thread waiting 
  for @{text "cs"}, therefore, after the @{text "V"}-operation, 
  it will become free; otherwise (represented 
  by @{text "valid_trace_v_n"}), one thread 
  will be picked from those in @{text "rest"} to take 
  over @{text "cs"}.
*}

locale valid_trace_v_e = valid_trace_v +
  assumes rest_nil: "rest = []"

locale valid_trace_v_n = valid_trace_v +
  assumes rest_nnl: "rest \<noteq> []"
begin

text {* 
  The following @{text "taker"} is the thread to 
  take over @{text "cs"}. 
*}
  definition "taker = hd wq'"

end


locale valid_trace_set = valid_trace_e + 
  fixes th prio
  assumes is_set: "e = Set th prio"

context valid_trace
begin

text {*
  Induction rule introduced to easy the 
  derivation of properties for valid trace @{term "s"}.
  One more premises, namely @{term "valid_trace_e s e"}
  is added, so that an interpretation of 
  @{text "valid_trace_e"} can be instantiated 
  so that all properties derived so far becomes 
  available in the proof of induction step.

  You will see its use in the proofs that follows.
*}
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

text {*
  The following lemma says that if @{text "s"} is a valid state, so 
  is its any postfix. Where @{term "monent t s"} is the postfix of 
  @{term "s"} with length @{term "t"}.
*}
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
end

text {*
  The following locale @{text "valid_moment"} is to inherit the properties 
  derived on any valid state to the prefix of it, with length @{text "i"}.
*}
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)

locale valid_moment_e = valid_moment +
  assumes less_i: "i < length s"
begin
  definition "next_e  = hd (moment (Suc i) s)"

  lemma trace_e: 
    "moment (Suc i) s = next_e#moment i s"
   proof -
    from less_i have "Suc i \<le> length s" by auto
    from moment_plus[OF this, folded next_e_def]
    show ?thesis .
   qed

end

sublocale valid_moment_e < vat_moment_e!: valid_trace_e "moment i s" "next_e"
  using vt_moment[of "Suc i", unfolded trace_e]
  by (unfold_locales, simp)

section {* Distinctiveness of waiting queues *}

context valid_trace_create
begin

lemma wq_kept [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_kept [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_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 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_kept [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  finite_threads:
  shows "finite (threads s)"
  using vt by (induct) (auto elim: step.cases)

lemma finite_readys [simp]: "finite (readys s)"
  using finite_threads readys_threads rev_finite_subset by blast

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

section {* Waiting queues and threads *}

context valid_trace_e
begin

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)

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)

end

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) distinct_rest: "distinct rest"
  by (simp add: distinct_tl rest_def wq_distinct)

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 

section {* RAG and threads *}

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 rg_RAG_threads: 
  assumes "(Th th) \<in> Range (RAG s)"
  shows "th \<in> threads s"
  using assms
  by (unfold s_RAG_def cs_waiting_def cs_holding_def, 
       auto intro:wq_threads)

lemma RAG_threads:
  assumes "(Th th) \<in> Field (RAG s)"
  shows "th \<in> threads s"
  using assms
  by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)

end

section {* The change of @{term RAG} *}

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 (in valid_trace_set) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"
   by (unfold is_set s_RAG_def s_waiting_def wq_def, simp add:Let_def)

lemma (in valid_trace_create) RAG_unchanged [simp]: "(RAG (e # s)) = RAG s"
 by (unfold is_create s_RAG_def s_waiting_def wq_def, simp add:Let_def)

lemma (in valid_trace_exit) RAG_unchanged[simp]: "(RAG (e # s)) = RAG s"
  by (unfold is_exit s_RAG_def s_waiting_def wq_def, simp add:Let_def)

context valid_trace_v
begin

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 set_wq': "set wq' = set rest"
  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 set_wq' by simp

lemma runing_th_s:
  shows "th \<in> runing s"
proof -
  from pip_e[unfolded is_v]
  show ?thesis by (cases, simp)
qed

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 

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 

  
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

lemma 
  finite_RAG_kept:
  assumes "finite (RAG s)"
  shows "finite (RAG (e#s))"
proof(cases "rest = []")
  case True
  interpret vt: valid_trace_v_e using True
    by (unfold_locales, simp)
  show ?thesis using assms
    by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
next
  case False
  interpret vt: valid_trace_v_n using False
    by (unfold_locales, simp)
  show ?thesis using assms
    by  (unfold RAG_es vt.waiting_set_eq vt.holding_set_eq, simp)
qed

end

context valid_trace_p
begin

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 

lemma (in valid_trace_p) 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

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_w
begin

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

section {* Finiteness of RAG *}

context valid_trace
begin

lemma finite_RAG:
  shows "finite (RAG s)"
proof(induct rule:ind)
  case Nil
  show ?case 
  by (auto simp: s_RAG_def cs_waiting_def 
                   cs_holding_def wq_def acyclic_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 by simp
  next
    case (Exit th)
    interpret vt: valid_trace_exit s e th using Exit
      by (unfold_locales, simp)
    show ?thesis using Cons by simp
  next
    case (P th cs)
    interpret vt: valid_trace_p s e th cs using P
      by (unfold_locales, simp)
    show ?thesis using Cons using vt.RAG_es by auto 
  next
    case (V th cs)
    interpret vt: valid_trace_v s e th cs using V
      by (unfold_locales, simp)
    show ?thesis using Cons by (simp add: vt.finite_RAG_kept) 
  next
    case (Set th prio)
    interpret vt: valid_trace_set s e th prio using Set
      by (unfold_locales, simp)
    show ?thesis using Cons by simp
  qed
qed
end

section {* RAG is acyclic *}

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.
*}


context valid_trace
begin

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" 
    interpret ve2: valid_moment_e _ t2 using lt2
     by (unfold_locales, simp)
    let ?e = ve2.next_e
    have "t2 < ?t3" by simp
    from nn2 [rule_format, OF this] and ve2.trace_e
    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 ?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 
          thus ?thesis
            using True h2 ve2.vat_moment_e.wq_out_inv by blast 
        qed
        thus ?thesis
          using step.cases ve2.vat_moment_e.pip_e by auto 
      next
        case False
        hence "?e = P thread cs2"
          using h1 ve2.vat_moment_e.wq_in_inv by blast 
        thus ?thesis
          using step.cases ve2.vat_moment_e.pip_e 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"
      interpret ve2: valid_moment_e _ t2 using lt2
        by (unfold_locales, simp)
      let ?e = ve2.next_e
      have "t2 < ?t3" by simp
      from nn2 [rule_format, OF this] and ve2.trace_e
      have h1: "thread \<in> set (wq (?e#moment t2 s) cs2)" by auto
      have lt_2: "t2 < ?t3" by simp
      from nn2 [rule_format, OF this] and ve2.trace_e
      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], unfolded ve2.trace_e[folded eq_12]] 
           eq_12[symmetric]
      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 "?e = V thread cs2 \<or> ?e = P thread cs2"
        using h1 h2 np2 ve2.vat_moment_e.wq_in_inv 
              ve2.vat_moment_e.wq_out_inv by blast
      moreover have "?e = V thread cs1 \<or> ?e = P thread cs1"
        using eq_12 g1 g2 np1 ve2.vat_moment_e.wq_in_inv 
              ve2.vat_moment_e.wq_out_inv by blast
      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

lemma (in valid_trace_v)
  preced_es [simp]: "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_s_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

end


lemma (in valid_trace_v_n) finite_waiting_set:
  "finite {(Th th', Cs cs) |th'. next_th s th cs th'}"
    by (simp add: waiting_set_eq)

lemma (in valid_trace_v_n) finite_holding_set:
  "finite {(Cs cs, Th th') |th'. next_th s th cs th'}"
    by (simp add: holding_set_eq)

lemma (in valid_trace_v_e) finite_waiting_set:
  "finite {(Th th', Cs cs) |th'. next_th s th cs th'}"
    by (simp add: waiting_set_eq)

lemma (in valid_trace_v_e) finite_holding_set:
  "finite {(Cs cs, Th th') |th'. next_th s th cs th'}"
    by (simp add: holding_set_eq)


context valid_trace_v_e
begin 

lemma 
  acylic_RAG_kept:
  assumes "acyclic (RAG s)"
  shows "acyclic (RAG (e#s))"
proof(rule acyclic_subset[OF assms])
  show "RAG (e # s) \<subseteq> RAG s"
      by (unfold RAG_es waiting_set_eq holding_set_eq, auto)
qed

end

context valid_trace_v_n
begin 

lemma waiting_taker: "waiting s taker cs"
  apply (unfold s_waiting_def, fold wq_def, unfold wq_s_cs taker_def)
  using eq_wq' th'_in_inv wq'_def by fastforce

lemma 
  acylic_RAG_kept:
  assumes "acyclic (RAG s)"
  shows "acyclic (RAG (e#s))"
proof -
  have "acyclic ((RAG s - {(Cs cs, Th th)} - {(Th taker, Cs cs)}) \<union> 
                 {(Cs cs, Th taker)})" (is "acyclic (?A \<union> _)")
  proof -
    from assms
    have "acyclic ?A"
       by (rule acyclic_subset, auto)
    moreover have "(Th taker, Cs cs) \<notin> ?A^*"
    proof
      assume otherwise: "(Th taker, Cs cs) \<in> ?A^*"
      hence "(Th taker, Cs cs) \<in> ?A^+"
        by (unfold rtrancl_eq_or_trancl, auto)
      from tranclD[OF this]
      obtain cs' where h: "(Th taker, Cs cs') \<in> ?A" 
                          "(Th taker, Cs cs') \<in> RAG s"
        by (unfold s_RAG_def, auto)
      from this(2) have "waiting s taker cs'" 
        by (unfold s_RAG_def, fold waiting_eq, auto)
      from waiting_unique[OF this waiting_taker] 
      have "cs' = cs" .
      from h(1)[unfolded this] show False by auto
    qed
    ultimately show ?thesis by auto
  qed
  thus ?thesis 
    by (unfold RAG_es waiting_set_eq holding_set_eq, simp)
qed

end

context valid_trace_p_h
begin

lemma 
  acylic_RAG_kept:
  assumes "acyclic (RAG s)"
  shows "acyclic (RAG (e#s))"
proof -
  have "acyclic (RAG s \<union> {(Cs cs, Th th)})" (is "acyclic (?A \<union> _)") 
  proof -
    from assms
    have "acyclic ?A"
       by (rule acyclic_subset, auto)
    moreover have "(Th th, Cs cs) \<notin> ?A^*"
    proof
      assume otherwise: "(Th th, Cs cs) \<in> ?A^*"
      hence "(Th th, Cs cs) \<in> ?A^+"
        by (unfold rtrancl_eq_or_trancl, auto)
      from tranclD[OF this]
      obtain cs' where h: "(Th th, Cs cs') \<in> RAG s"
        by (unfold s_RAG_def, auto)
      hence "waiting s th cs'" 
        by (unfold s_RAG_def, fold waiting_eq, auto)
      with th_not_waiting show False by auto 
    qed
    ultimately show ?thesis by auto
  qed
  thus ?thesis by (unfold RAG_es, simp)
qed

end

context valid_trace_p_w
begin

lemma 
  acylic_RAG_kept:
  assumes "acyclic (RAG s)"
  shows "acyclic (RAG (e#s))"
proof -
  have "acyclic (RAG s \<union> {(Th th, Cs cs)})" (is "acyclic (?A \<union> _)") 
  proof -
    from assms
    have "acyclic ?A"
       by (rule acyclic_subset, auto)
    moreover have "(Cs cs, Th th) \<notin> ?A^*"
    proof
      assume otherwise: "(Cs cs, Th th) \<in> ?A^*"
      from pip_e[unfolded is_p]
      show False
      proof(cases)
        case (thread_P)
        moreover from otherwise have "(Cs cs, Th th) \<in> ?A^+"
            by (unfold rtrancl_eq_or_trancl, auto)
        ultimately show ?thesis by auto
      qed
    qed
    ultimately show ?thesis by auto
  qed
  thus ?thesis by (unfold RAG_es, simp)
qed

end

context valid_trace
begin

lemma acyclic_RAG:
  shows "acyclic (RAG s)"
proof(induct rule:ind)
  case Nil
  show ?case 
  by (auto simp: s_RAG_def cs_waiting_def 
                   cs_holding_def wq_def acyclic_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 by simp 
  next
    case (Exit th)
    interpret vt: valid_trace_exit s e th using Exit
      by (unfold_locales, simp)
    show ?thesis using Cons by simp
  next
    case (P th cs)
    interpret vt: valid_trace_p s e th cs using P
      by (unfold_locales, simp)
    show ?thesis
    proof(cases "wq s cs = []")
      case True
      then interpret vt_h: valid_trace_p_h s e th cs
        by (unfold_locales, simp)
      show ?thesis using Cons by (simp add: vt_h.acylic_RAG_kept) 
    next
      case False
      then interpret vt_w: valid_trace_p_w s e th cs
        by (unfold_locales, simp)
      show ?thesis using Cons by (simp add: vt_w.acylic_RAG_kept) 
    qed
  next
    case (V th cs)
    interpret vt: valid_trace_v s e th cs using V
      by (unfold_locales, simp)
    show ?thesis
    proof(cases "vt.rest = []")
      case True
      then interpret vt_e: valid_trace_v_e s e th cs
        by (unfold_locales, simp)
      show ?thesis by (simp add: Cons.hyps(2) vt_e.acylic_RAG_kept) 
    next
      case False
      then interpret vt_n: valid_trace_v_n s e th cs
        by (unfold_locales, simp)
      show ?thesis by (simp add: Cons.hyps(2) vt_n.acylic_RAG_kept) 
    qed
  next
    case (Set th prio)
    interpret vt: valid_trace_set s e th prio using Set
      by (unfold_locales, simp)
    show ?thesis using Cons by simp 
  qed
qed

end

section {* RAG is single-valued *}

context valid_trace
begin

lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
  apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
  by(auto elim:waiting_unique held_unique)

lemma sgv_RAG: "single_valued (RAG s)"
  using unique_RAG by (auto simp:single_valued_def)

end

section {* RAG is well-founded *}

context valid_trace
begin

lemma wf_RAG: "wf (RAG s)"
proof(rule finite_acyclic_wf)
  from finite_RAG show "finite (RAG s)" .
next
  from acyclic_RAG show "acyclic (RAG s)" .
qed

lemma wf_RAG_converse: 
  shows "wf ((RAG s)^-1)"
proof(rule finite_acyclic_wf_converse)
  from finite_RAG 
  show "finite (RAG s)" .
next
  from acyclic_RAG
  show "acyclic (RAG s)" .
qed

end

section {* RAG forms a forest (or tree) *}

context valid_trace
begin

lemma rtree_RAG: "rtree (RAG s)"
  using sgv_RAG acyclic_RAG
  by (unfold rtree_def rtree_axioms_def sgv_def, auto)

end

sublocale valid_trace < rtree_RAG: rtree "RAG s"
  using rtree_RAG .

sublocale valid_trace < fsbtRAGs : fsubtree "RAG s"
proof -
  show "fsubtree (RAG s)"
  proof(intro_locales)
    show "fbranch (RAG s)" using finite_fbranchI[OF finite_RAG] .
  next
    show "fsubtree_axioms (RAG s)"
    proof(unfold fsubtree_axioms_def)
      from wf_RAG show "wf (RAG s)" .
    qed
  qed
qed


section {* Derived properties for parts of RAG *}

context valid_trace
begin

lemma acyclic_tRAG: "acyclic (tRAG s)"
proof(unfold tRAG_def, rule acyclic_compose)
  show "acyclic (RAG s)" using acyclic_RAG .
next
  show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto
next
  show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto
qed

lemma sgv_wRAG: "single_valued (wRAG s)"
  using waiting_unique
  by (unfold single_valued_def wRAG_def, auto)

lemma sgv_hRAG: "single_valued (hRAG s)"
  using held_unique 
  by (unfold single_valued_def hRAG_def, auto)

lemma sgv_tRAG: "single_valued (tRAG s)"
  by (unfold tRAG_def, rule single_valued_relcomp, 
              insert sgv_wRAG sgv_hRAG, auto)

end

sublocale valid_trace < rtree_s: rtree "tRAG s"
proof(unfold_locales)
  from sgv_tRAG show "single_valued (tRAG s)" .
next
  from acyclic_tRAG show "acyclic (tRAG s)" .
qed

sublocale valid_trace < fsbttRAGs: fsubtree "tRAG s"
proof -
  have "fsubtree (tRAG s)"
  proof -
    have "fbranch (tRAG s)"
    proof(unfold tRAG_def, rule fbranch_compose)
        show "fbranch (wRAG s)"
        proof(rule finite_fbranchI)
           from finite_RAG show "finite (wRAG s)"
           by (unfold RAG_split, auto)
        qed
    next
        show "fbranch (hRAG s)"
        proof(rule finite_fbranchI)
           from finite_RAG 
           show "finite (hRAG s)" by (unfold RAG_split, auto)
        qed
    qed
    moreover have "wf (tRAG s)"
    proof(rule wf_subset)
      show "wf (RAG s O RAG s)" using wf_RAG
        by (fold wf_comp_self, simp)
    next
      show "tRAG s \<subseteq> (RAG s O RAG s)"
        by (unfold tRAG_alt_def, auto)
    qed
    ultimately show ?thesis
      by (unfold fsubtree_def fsubtree_axioms_def,auto)
  qed
  from this[folded tRAG_def] show "fsubtree (tRAG s)" .
qed

lemma tRAG_nodeE:
  assumes "(n1, n2) \<in> tRAG s"
  obtains th1 th2 where "n1 = Th th1" "n2 = Th th2"
  using assms
  by (auto simp: tRAG_def wRAG_def hRAG_def)

lemma tRAG_ancestorsE:
  assumes "x \<in> ancestors (tRAG s) u"
  obtains th where "x = Th th"
proof -
  from assms have "(u, x) \<in> (tRAG s)^+" 
      by (unfold ancestors_def, auto)
  from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
  then obtain th where "x = Th th"
    by (unfold tRAG_alt_def, auto)
  from that[OF this] show ?thesis .
qed
                   
lemma subtree_nodeE:
  assumes "n \<in> subtree (tRAG s) (Th th)"
  obtains th1 where "n = Th th1"
proof -
  show ?thesis
  proof(rule subtreeE[OF assms])
    assume "n = Th th"
    from that[OF this] show ?thesis .
  next
    assume "Th th \<in> ancestors (tRAG s) n"
    hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)
    hence "\<exists> th1. n = Th th1"
    proof(induct)
      case (base y)
      from tRAG_nodeE[OF this] show ?case by metis
    next
      case (step y z)
      thus ?case by auto
    qed
    with that show ?thesis by auto
  qed
qed

lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"
proof -
  have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*" 
    by (rule rtrancl_mono, auto simp:RAG_split)
  also have "... \<subseteq> ((RAG s)^*)^*"
    by (rule rtrancl_mono, auto)
  also have "... = (RAG s)^*" by simp
  finally show ?thesis by (unfold tRAG_def, simp)
qed

lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"
proof -
  { fix a
    assume "a \<in> subtree (tRAG s) x"
    hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)
    with tRAG_star_RAG
    have "(a, x) \<in> (RAG s)^*" by auto
    hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def)
  } thus ?thesis by auto
qed

lemma tRAG_trancl_eq:
   "{th'. (Th th', Th th)  \<in> (tRAG s)^+} = 
    {th'. (Th th', Th th)  \<in> (RAG s)^+}"
   (is "?L = ?R")
proof -
  { fix th'
    assume "th' \<in> ?L"
    hence "(Th th', Th th) \<in> (tRAG s)^+" by auto
    from tranclD[OF this]
    obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto
    from tRAG_subtree_RAG and this(2)
    have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG) 
    moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto 
    ultimately have "th' \<in> ?R"  by auto 
  } moreover 
  { fix th'
    assume "th' \<in> ?R"
    hence "(Th th', Th th) \<in> (RAG s)^+" by (auto)
    from plus_rpath[OF this]
    obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto
    hence "(Th th', Th th) \<in> (tRAG s)^+"
    proof(induct xs arbitrary:th' th rule:length_induct)
      case (1 xs th' th)
      then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto)
      show ?case
      proof(cases "xs1")
        case Nil
        from 1(2)[unfolded Cons1 Nil]
        have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .
        hence "(Th th', x1) \<in> (RAG s)" 
          by (cases, auto)
        then obtain cs where "x1 = Cs cs" 
              by (unfold s_RAG_def, auto)
        from rpath_nnl_lastE[OF rp[unfolded this]]
        show ?thesis by auto
      next
        case (Cons x2 xs2)
        from 1(2)[unfolded Cons1[unfolded this]]
        have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" .
        from rpath_edges_on[OF this]
        have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" .
        have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)"
            by (simp add: edges_on_unfold)
        with eds have rg1: "(Th th', x1) \<in> RAG s" by auto
        then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto)
        have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)"
            by (simp add: edges_on_unfold)
        from this eds
        have rg2: "(x1, x2) \<in> RAG s" by auto
        from this[unfolded eq_x1] 
        obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto)
        from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]
        have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto)
        from rp have "rpath (RAG s) x2 xs2 (Th th)"
           by  (elim rpath_ConsE, simp)
        from this[unfolded eq_x2] have rp': "rpath (RAG s) (Th th1) xs2 (Th th)" .
        show ?thesis
        proof(cases "xs2 = []")
          case True
          from rpath_nilE[OF rp'[unfolded this]]
          have "th1 = th" by auto
          from rt1[unfolded this] show ?thesis by auto
        next
          case False
          from 1(1)[rule_format, OF _ rp' this, unfolded Cons1 Cons]
          have "(Th th1, Th th) \<in> (tRAG s)\<^sup>+" by simp
          with rt1 show ?thesis by auto
        qed
      qed
    qed
    hence "th' \<in> ?L" by auto
  } ultimately show ?thesis by blast
qed

lemma tRAG_trancl_eq_Th:
   "{Th th' | th'. (Th th', Th th)  \<in> (tRAG s)^+} = 
    {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}"
    using tRAG_trancl_eq by auto


lemma tRAG_Field:
  "Field (tRAG s) \<subseteq> Field (RAG s)"
  by (unfold tRAG_alt_def Field_def, auto)

lemma tRAG_mono:
  assumes "RAG s' \<subseteq> RAG s"
  shows "tRAG s' \<subseteq> tRAG s"
  using assms 
  by (unfold tRAG_alt_def, auto)

lemma tRAG_subtree_eq: 
   "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th'  \<in> (subtree (RAG s) (Th th))}"
   (is "?L = ?R")
proof -
  { fix n 
    assume h: "n \<in> ?L"
    hence "n \<in> ?R"
    by (smt mem_Collect_eq subsetCE subtree_def subtree_nodeE tRAG_subtree_RAG) 
  } moreover {
    fix n
    assume "n \<in> ?R"
    then obtain th' where h: "n = Th th'" "(Th th', Th th) \<in> (RAG s)^*"
      by (auto simp:subtree_def)
    from rtranclD[OF this(2)]
    have "n \<in> ?L"
    proof
      assume "Th th' \<noteq> Th th \<and> (Th th', Th th) \<in> (RAG s)\<^sup>+"
      with h have "n \<in> {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}" by auto
      thus ?thesis using subtree_def tRAG_trancl_eq by fastforce
    qed (insert h, auto simp:subtree_def)
  } ultimately show ?thesis by auto
qed

lemma threads_set_eq: 
   "the_thread ` (subtree (tRAG s) (Th th)) = 
                  {th'. Th th' \<in> (subtree (RAG s) (Th th))}" (is "?L = ?R")
   by (auto intro:rev_image_eqI simp:tRAG_subtree_eq)

lemma dependants_alt_def:
  "dependants s th = {th'. (Th th', Th th) \<in> (tRAG s)^+}"
  by (metis eq_RAG s_dependants_def tRAG_trancl_eq)

lemma dependants_alt_def1:
  "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"
  using dependants_alt_def tRAG_trancl_eq by auto

section {* Chain to readys *}

context valid_trace
begin

lemma chain_building:
  assumes "node \<in> Domain (RAG s)"
  obtains th' where "th' \<in> readys s" "(node, Th th') \<in> (RAG s)^+"
proof -
  from assms have "node \<in> Range ((RAG s)^-1)" by auto
  from wf_base[OF wf_RAG_converse this]
  obtain b where h_b: "(b, node) \<in> ((RAG s)\<inverse>)\<^sup>+" "\<forall>c. (c, b) \<notin> (RAG s)\<inverse>" by auto
  obtain th' where eq_b: "b = Th th'"
  proof(cases b)
    case (Cs cs)
    from h_b(1)[unfolded trancl_converse] 
    have "(node, b) \<in> ((RAG s)\<^sup>+)" by auto
    from tranclE[OF this]
    obtain n where "(n, b) \<in> RAG s" by auto
    from this[unfolded Cs]
    obtain th1 where "waiting s th1 cs"
      by (unfold s_RAG_def, fold waiting_eq, auto)
    from waiting_holding[OF this]
    obtain th2 where "holding s th2 cs" .
    hence "(Cs cs, Th th2) \<in> RAG s"
      by (unfold s_RAG_def, fold holding_eq, auto)
    with h_b(2)[unfolded Cs, rule_format]
    have False by auto
    thus ?thesis by auto
  qed auto
  have "th' \<in> readys s" 
  proof -
    from h_b(2)[unfolded eq_b]
    have "\<forall>cs. \<not> waiting s th' cs"
      by (unfold s_RAG_def, fold waiting_eq, auto)
    moreover have "th' \<in> threads s"
    proof(rule rg_RAG_threads)
      from tranclD[OF h_b(1), unfolded eq_b]
      obtain z where "(z, Th th') \<in> (RAG s)" by auto
      thus "Th th' \<in> Range (RAG s)" by auto
    qed
    ultimately show ?thesis by (auto simp:readys_def)
  qed
  moreover have "(node, Th th') \<in> (RAG s)^+" 
    using h_b(1)[unfolded trancl_converse] eq_b by auto
  ultimately show ?thesis using that by metis
qed

text {* \noindent
  The following is just an instance of @{text "chain_building"}.
*}                    
lemma th_chain_to_ready:
  assumes th_in: "th \<in> threads s"
  shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (Th th, Th th') \<in> (RAG s)^+)"
proof(cases "th \<in> readys s")
  case True
  thus ?thesis by auto
next
  case False
  from False and th_in have "Th th \<in> Domain (RAG s)" 
    by (auto simp:readys_def s_waiting_def s_RAG_def wq_def cs_waiting_def Domain_def)
  from chain_building [rule_format, OF this]
  show ?thesis by auto
qed

lemma finite_subtree_threads:
    "finite {th'. Th th' \<in> subtree (RAG s) (Th th)}" (is "finite ?A")
proof -
  have "?A = the_thread ` {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}"
        by (auto, insert image_iff, fastforce)
  moreover have "finite {Th th' | th' . Th th' \<in> subtree (RAG s) (Th th)}"
        (is "finite ?B")
  proof -
     have "?B = (subtree (RAG s) (Th th)) \<inter> {Th th' | th'. True}"
      by auto
     moreover have "... \<subseteq> (subtree (RAG s) (Th th))" by auto
     moreover have "finite ..." by (simp add: fsbtRAGs.finite_subtree) 
     ultimately show ?thesis by auto
  qed
  ultimately show ?thesis by auto
qed

lemma runing_unique:
  assumes runing_1: "th1 \<in> runing s"
  and runing_2: "th2 \<in> runing s"
  shows "th1 = th2"
proof -
  from runing_1 and runing_2 have "cp s th1 = cp s th2"
    unfolding runing_def by auto
  from this[unfolded cp_alt_def]
  have eq_max: 
    "Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th1)}) =
     Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th2)})" 
        (is "Max ?L = Max ?R") .
  have "Max ?L \<in> ?L"
  proof(rule Max_in)
    show "finite ?L" by (simp add: finite_subtree_threads) 
  next
    show "?L \<noteq> {}" using subtree_def by fastforce 
  qed
  then obtain th1' where 
    h_1: "Th th1' \<in> subtree (RAG s) (Th th1)" "the_preced s th1' = Max ?L"
    by auto
  have "Max ?R \<in> ?R"
  proof(rule Max_in)
    show "finite ?R" by (simp add: finite_subtree_threads)
  next
    show "?R \<noteq> {}" using subtree_def by fastforce 
  qed
  then obtain th2' where 
    h_2: "Th th2' \<in> subtree (RAG s) (Th th2)" "the_preced s th2' = Max ?R"
    by auto
  have "th1' = th2'"
  proof(rule preced_unique)
    from h_1(1)
    show "th1' \<in> threads s"
    proof(cases rule:subtreeE)
      case 1
      hence "th1' = th1" by simp
      with runing_1 show ?thesis by (auto simp:runing_def readys_def)
    next
      case 2
      from this(2)
      have "(Th th1', Th th1) \<in> (RAG s)^+" by (auto simp:ancestors_def)
      from tranclD[OF this]
      have "(Th th1') \<in> Domain (RAG s)" by auto
      from dm_RAG_threads[OF this] show ?thesis .
    qed
  next
    from h_2(1)
    show "th2' \<in> threads s"
    proof(cases rule:subtreeE)
      case 1
      hence "th2' = th2" by simp
      with runing_2 show ?thesis by (auto simp:runing_def readys_def)
    next
      case 2
      from this(2)
      have "(Th th2', Th th2) \<in> (RAG s)^+" by (auto simp:ancestors_def)
      from tranclD[OF this]
      have "(Th th2') \<in> Domain (RAG s)" by auto
      from dm_RAG_threads[OF this] show ?thesis .
    qed
  next
    have "the_preced s th1' = the_preced s th2'" 
     using eq_max h_1(2) h_2(2) by metis
    thus "preced th1' s = preced th2' s" by (simp add:the_preced_def)
  qed
  from h_1(1)[unfolded this]
  have star1: "(Th th2', Th th1) \<in> (RAG s)^*" by (auto simp:subtree_def)
  from h_2(1)[unfolded this]
  have star2: "(Th th2', Th th2) \<in> (RAG s)^*" by (auto simp:subtree_def)
  from star_rpath[OF star1] obtain xs1 
    where rp1: "rpath (RAG s) (Th th2') xs1 (Th th1)"
    by auto
  from star_rpath[OF star2] obtain xs2 
    where rp2: "rpath (RAG s) (Th th2') xs2 (Th th2)"
    by auto
  from rp1 rp2
  show ?thesis
  proof(cases)
    case (less_1 xs')
    moreover have "xs' = []"
    proof(rule ccontr)
      assume otherwise: "xs' \<noteq> []"
      from rpath_plus[OF less_1(3) this]
      have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" .
      from tranclD[OF this]
      obtain cs where "waiting s th1 cs"
        by (unfold s_RAG_def, fold waiting_eq, auto)
      with runing_1 show False
        by (unfold runing_def readys_def, auto)
    qed
    ultimately have "xs2 = xs1" by simp
    from rpath_dest_eq[OF rp1 rp2[unfolded this]]
    show ?thesis by simp
  next
    case (less_2 xs')
    moreover have "xs' = []"
    proof(rule ccontr)
      assume otherwise: "xs' \<noteq> []"
      from rpath_plus[OF less_2(3) this]
      have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" .
      from tranclD[OF this]
      obtain cs where "waiting s th2 cs"
        by (unfold s_RAG_def, fold waiting_eq, auto)
      with runing_2 show False
        by (unfold runing_def readys_def, auto)
    qed
    ultimately have "xs2 = xs1" by simp
    from rpath_dest_eq[OF rp1 rp2[unfolded this]]
    show ?thesis by simp
  qed
qed

lemma card_runing: "card (runing s) \<le> 1"
proof(cases "runing s = {}")
  case True
  thus ?thesis by auto
next
  case False
  then obtain th where [simp]: "th \<in> runing s" by auto
  from runing_unique[OF this]
  have "runing s = {th}" by auto
  thus ?thesis by auto
qed

end


section {* Relating @{term cp} and @{term the_preced} and @{term preced} *}

context valid_trace
begin

lemma le_cp:
  shows "preced th s \<le> cp s th"
  proof(unfold cp_alt_def, rule Max_ge)
    show "finite (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})"
      by (simp add: finite_subtree_threads)
  next
    show "preced th s \<in> the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}"
      by (simp add: subtree_def the_preced_def)   
  qed


lemma cp_le:
  assumes th_in: "th \<in> threads s"
  shows "cp s th \<le> Max (the_preced s ` threads s)"
proof(unfold cp_alt_def, rule Max_f_mono)
  show "finite (threads s)" by (simp add: finite_threads) 
next
  show " {th'. Th th' \<in> subtree (RAG s) (Th th)} \<noteq> {}"
    using subtree_def by fastforce
next
  show "{th'. Th th' \<in> subtree (RAG s) (Th th)} \<subseteq> threads s"
    using assms
    by (smt Domain.DomainI dm_RAG_threads mem_Collect_eq 
        node.inject(1) rtranclD subsetI subtree_def trancl_domain) 
qed

lemma max_cp_eq: 
  shows "Max ((cp s) ` threads s) = Max (the_preced s ` threads s)"
  (is "?L = ?R")
proof -
  have "?L \<le> ?R" 
  proof(cases "threads s = {}")
    case False
    show ?thesis 
      by (rule Max.boundedI, 
          insert cp_le, 
          auto simp:finite_threads False)
  qed auto
  moreover have "?R \<le> ?L"
    by (rule Max_fg_mono, 
        simp add: finite_threads,
        simp add: le_cp the_preced_def)
  ultimately show ?thesis by auto
qed

end

section {* Relating @{term cntP}, @{term cntV}, @{term cntCS} and @{term pvD} *}

context valid_trace_p_w
begin

lemma holding_s_holder: "holding s holder cs"
  by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)

lemma holding_es_holder: "holding (e#s) holder cs"
  by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto)

lemma holdents_es:
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R") 
proof -
  { fix cs'
    assume "cs' \<in> ?L"
    hence h: "holding (e#s) th' cs'" by (auto simp:holdents_def)
    have "holding s th' cs'"
    proof(cases "cs' = cs")
      case True
      from held_unique[OF h[unfolded True] holding_es_holder]
      have "th' = holder" .
      thus ?thesis 
        by (unfold True holdents_def, insert holding_s_holder, simp)
    next
      case False
      hence "wq (e#s) cs' = wq s cs'" by simp
      from h[unfolded s_holding_def, folded wq_def, unfolded this]
      show ?thesis
       by (unfold s_holding_def, fold wq_def, auto)
    qed 
    hence "cs' \<in> ?R" by (auto simp:holdents_def)
  } moreover {
    fix cs'
    assume "cs' \<in> ?R"
    hence h: "holding s th' cs'" by (auto simp:holdents_def)
    have "holding (e#s) th' cs'"
    proof(cases "cs' = cs")
      case True
      from held_unique[OF h[unfolded True] holding_s_holder]
      have "th' = holder" .
      thus ?thesis 
        by (unfold True holdents_def, insert holding_es_holder, simp)
    next
      case False
      hence "wq s cs' = wq (e#s) cs'" by simp
      from h[unfolded s_holding_def, folded wq_def, unfolded this]
      show ?thesis
       by (unfold s_holding_def, fold wq_def, auto)
    qed 
    hence "cs' \<in> ?L" by (auto simp:holdents_def)
  } ultimately show ?thesis by auto
qed

lemma cntCS_es_th[simp]: "cntCS (e#s) th' = cntCS s th'"
 by (unfold cntCS_def holdents_es, simp)

lemma th_not_ready_es: 
  shows "th \<notin> readys (e#s)"
  using waiting_es_th_cs 
  by (unfold readys_def, auto)

end
  
lemma (in valid_trace) finite_holdents: "finite (holdents s th)"
  by (unfold holdents_alt_def, insert fsbtRAGs.finite_children, auto)

context valid_trace_p 
begin

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 waiting_neq_th: 
  assumes "waiting s t c"
  shows "t \<noteq> th"
  using assms using th_not_waiting by blast 

end

context valid_trace_p_h
begin

lemma th_not_waiting':
  "\<not> waiting (e#s) th cs'"
proof(cases "cs' = cs")
  case True
  show ?thesis
    by (unfold True s_waiting_def, fold wq_def, unfold wq_es_cs', auto)
next
  case False
  from th_not_waiting[of cs', unfolded s_waiting_def, folded wq_def]
  show ?thesis
    by (unfold s_waiting_def, fold wq_def, insert False, simp)
qed

lemma ready_th_es: 
  shows "th \<in> readys (e#s)"
  using th_not_waiting'
  by (unfold readys_def, insert live_th_es, auto)

lemma holdents_es_th:
  "holdents (e#s) th = (holdents s th) \<union> {cs}" (is "?L = ?R")
proof -
  { fix cs'
    assume "cs' \<in> ?L" 
    hence "holding (e#s) th cs'"
      by (unfold holdents_def, auto)
    hence "cs' \<in> ?R"
     by (cases rule:holding_esE, auto simp:holdents_def)
  } moreover {
    fix cs'
    assume "cs' \<in> ?R"
    hence "holding s th cs' \<or> cs' = cs" 
      by (auto simp:holdents_def)
    hence "cs' \<in> ?L"
    proof
      assume "holding s th cs'"
      from holding_kept[OF this]
      show ?thesis by (auto simp:holdents_def)
    next
      assume "cs' = cs"
      thus ?thesis using holding_es_th_cs
        by (unfold holdents_def, auto)
    qed
  } ultimately show ?thesis by auto
qed

lemma cntCS_es_th: "cntCS (e#s) th = cntCS s th + 1"
proof -
  have "card (holdents s th \<union> {cs}) = card (holdents s th) + 1"
  proof(subst card_Un_disjoint)
    show "holdents s th \<inter> {cs} = {}"
      using not_holding_s_th_cs by (auto simp:holdents_def)
  qed (auto simp:finite_holdents)
  thus ?thesis
   by (unfold cntCS_def holdents_es_th, simp)
qed

lemma no_holder: 
  "\<not> holding s th' cs"
proof
  assume otherwise: "holding s th' cs"
  from this[unfolded s_holding_def, folded wq_def, unfolded we]
  show False by auto
qed

lemma holdents_es_th':
  assumes "th' \<noteq> th"
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
  { fix cs'
    assume "cs' \<in> ?L"
    hence h_e: "holding (e#s) th' cs'" by (auto simp:holdents_def)
    have "cs' \<noteq> cs"
    proof
      assume "cs' = cs"
      from held_unique[OF h_e[unfolded this] holding_es_th_cs]
      have "th' = th" .
      with assms show False by simp
    qed
    from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]]
    have "th' \<in> set (wq s cs') \<and> th' = hd (wq s cs')" .
    hence "cs' \<in> ?R" 
      by (unfold holdents_def s_holding_def, fold wq_def, auto)
  } moreover {
    fix cs'
    assume "cs' \<in> ?R"
    hence "holding s th' cs'" by (auto simp:holdents_def)
    from holding_kept[OF this]
    have "holding (e # s) th' cs'" .
    hence "cs' \<in> ?L"
      by (unfold holdents_def, auto)
  } ultimately show ?thesis by auto
qed

lemma cntCS_es_th'[simp]: 
  assumes "th' \<noteq> th"
  shows "cntCS (e#s) th' = cntCS s th'"
  by (unfold cntCS_def holdents_es_th'[OF assms], simp)

end

context valid_trace_p
begin

lemma readys_kept1: 
  assumes "th' \<noteq> th"
  and "th' \<in> readys (e#s)"
  shows "th' \<in> readys s"
proof -
  { fix cs'
    assume wait: "waiting s th' cs'"
    have n_wait: "\<not> waiting (e#s) th' cs'" 
        using assms(2)[unfolded readys_def] by auto
    have False
    proof(cases "cs' = cs")
      case False
      with n_wait wait
      show ?thesis 
        by (unfold s_waiting_def, fold wq_def, auto)
    next
      case True
      show ?thesis
      proof(cases "wq s cs = []")
        case True
        then interpret vt: valid_trace_p_h
          by (unfold_locales, simp)
        show ?thesis using n_wait wait waiting_kept by auto 
      next
        case False
        then interpret vt: valid_trace_p_w by (unfold_locales, simp)
        show ?thesis using n_wait wait waiting_kept by blast 
      qed
    qed
  } with assms(2) show ?thesis  
    by (unfold readys_def, auto)
qed

lemma readys_kept2: 
  assumes "th' \<noteq> th"
  and "th' \<in> readys s"
  shows "th' \<in> readys (e#s)"
proof -
  { fix cs'
    assume wait: "waiting (e#s) th' cs'"
    have n_wait: "\<not> waiting s th' cs'" 
        using assms(2)[unfolded readys_def] by auto
    have False
    proof(cases "cs' = cs")
      case False
      with n_wait wait
      show ?thesis 
        by (unfold s_waiting_def, fold wq_def, auto)
    next
      case True
      show ?thesis
      proof(cases "wq s cs = []")
        case True
        then interpret vt: valid_trace_p_h
          by (unfold_locales, simp)
        show ?thesis using n_wait vt.waiting_esE wait by blast 
      next
        case False
        then interpret vt: valid_trace_p_w by (unfold_locales, simp)
        show ?thesis using assms(1) n_wait vt.waiting_esE wait by auto 
      qed
    qed
  } with assms(2) show ?thesis  
    by (unfold readys_def, auto)
qed

lemma readys_simp [simp]:
  assumes "th' \<noteq> th"
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
  using readys_kept1[OF assms] readys_kept2[OF assms]
  by metis

lemma cnp_cnv_cncs_kept: (* ddd *)
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"
proof(cases "th' = th")
  case True
  note eq_th' = this
  show ?thesis
  proof(cases "wq s cs = []")
    case True
    then interpret vt: valid_trace_p_h by (unfold_locales, simp)
    show ?thesis
      using assms eq_th' is_p ready_th_s vt.cntCS_es_th vt.ready_th_es pvD_def by auto 
  next
    case False
    then interpret vt: valid_trace_p_w by (unfold_locales, simp)
    show ?thesis
      using add.commute add.left_commute assms eq_th' is_p live_th_s 
            ready_th_s vt.th_not_ready_es pvD_def
      apply (auto)
      by (fold is_p, simp)
  qed
next
  case False
  note h_False = False
  thus ?thesis
  proof(cases "wq s cs = []")
    case True
    then interpret vt: valid_trace_p_h by (unfold_locales, simp)
    show ?thesis using assms
      by (insert True h_False pvD_def, auto split:if_splits,unfold is_p, auto)
  next
    case False
    then interpret vt: valid_trace_p_w by (unfold_locales, simp)
    show ?thesis using assms
      by (insert False h_False pvD_def, auto split:if_splits,unfold is_p, auto)
  qed
qed

end


context valid_trace_v 
begin

lemma holding_th_cs_s: 
  "holding s th cs" 
 by  (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)

lemma th_ready_s [simp]: "th \<in> readys s"
  using runing_th_s
  by (unfold runing_def readys_def, auto)

lemma th_live_s [simp]: "th \<in> threads s"
  using th_ready_s by (unfold readys_def, auto)

lemma th_ready_es [simp]: "th \<in> readys (e#s)"
  using runing_th_s neq_t_th
  by (unfold is_v runing_def readys_def, auto)

lemma th_live_es [simp]: "th \<in> threads (e#s)"
  using th_ready_es by (unfold readys_def, auto)

lemma pvD_th_s[simp]: "pvD s th = 0"
  by (unfold pvD_def, simp)

lemma pvD_th_es[simp]: "pvD (e#s) th = 0"
  by (unfold pvD_def, simp)

lemma cntCS_s_th [simp]: "cntCS s th > 0"
proof -
  have "cs \<in> holdents s th" using holding_th_cs_s
    by (unfold holdents_def, simp)
  moreover have "finite (holdents s th)" using finite_holdents 
    by simp
  ultimately show ?thesis
    by (unfold cntCS_def, 
        auto intro!:card_gt_0_iff[symmetric, THEN iffD1])
qed

end

context valid_trace_v
begin

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 

end

context valid_trace_v_n
begin

lemma not_ready_taker_s[simp]: 
  "taker \<notin> readys s"
  using waiting_taker
  by (unfold readys_def, auto)

lemma taker_live_s [simp]: "taker \<in> threads s"
proof -
  have "taker \<in> set wq'" by (simp add: eq_wq') 
  from th'_in_inv[OF this]
  have "taker \<in> set rest" .
  hence "taker \<in> set (wq s cs)" by (simp add: wq_s_cs) 
  thus ?thesis using wq_threads by auto 
qed

lemma taker_live_es [simp]: "taker \<in> threads (e#s)"
  using taker_live_s threads_es by blast

lemma taker_ready_es [simp]:
  shows "taker \<in> readys (e#s)"
proof -
  { fix cs'
    assume "waiting (e#s) taker cs'"
    hence False
    proof(cases rule:waiting_esE)
      case 1
      thus ?thesis using waiting_taker waiting_unique by auto 
    qed simp
  } thus ?thesis by (unfold readys_def, auto)
qed

lemma neq_taker_th: "taker \<noteq> th"
  using th_not_waiting waiting_taker by blast 

lemma not_holding_taker_s_cs:
  shows "\<not> holding s taker cs"
  using holding_cs_eq_th neq_taker_th by auto

lemma holdents_es_taker:
  "holdents (e#s) taker = holdents s taker \<union> {cs}" (is "?L = ?R")
proof -
  { fix cs'
    assume "cs' \<in> ?L"
    hence "holding (e#s) taker cs'" by (auto simp:holdents_def)
    hence "cs' \<in> ?R"
    proof(cases rule:holding_esE)
      case 2
      thus ?thesis by (auto simp:holdents_def)
    qed auto
  } moreover {
    fix cs'
    assume "cs' \<in> ?R"
    hence "holding s taker cs' \<or> cs' = cs" by (auto simp:holdents_def)
    hence "cs' \<in> ?L" 
    proof
      assume "holding s taker cs'"
      hence "holding (e#s) taker cs'" 
          using holding_esI2 holding_taker by fastforce 
      thus ?thesis by (auto simp:holdents_def)
    next
      assume "cs' = cs"
      with holding_taker
      show ?thesis by (auto simp:holdents_def)
    qed
  } ultimately show ?thesis by auto
qed

lemma cntCS_es_taker [simp]: "cntCS (e#s) taker = cntCS s taker + 1"
proof -
  have "card (holdents s taker \<union> {cs}) = card (holdents s taker) + 1"
  proof(subst card_Un_disjoint)
    show "holdents s taker \<inter> {cs} = {}"
      using not_holding_taker_s_cs by (auto simp:holdents_def)
  qed (auto simp:finite_holdents)
  thus ?thesis 
    by (unfold cntCS_def, insert holdents_es_taker, simp)
qed

lemma pvD_taker_s[simp]: "pvD s taker = 1"
  by (unfold pvD_def, simp)

lemma pvD_taker_es[simp]: "pvD (e#s) taker = 0"
  by (unfold pvD_def, simp)  

lemma pvD_th_s[simp]: "pvD s th = 0"
  by (unfold pvD_def, simp)

lemma pvD_th_es[simp]: "pvD (e#s) th = 0"
  by (unfold pvD_def, simp)

lemma holdents_es_th:
  "holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R")
proof -
  { fix cs'
    assume "cs' \<in> ?L"
    hence "holding (e#s) th cs'" by (auto simp:holdents_def)
    hence "cs' \<in> ?R"
    proof(cases rule:holding_esE)
      case 2
      thus ?thesis by (auto simp:holdents_def)
    qed (insert neq_taker_th, auto)
  } moreover {
    fix cs'
    assume "cs' \<in> ?R"
    hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def)
    from holding_esI2[OF this]
    have "cs' \<in> ?L" by (auto simp:holdents_def)
  } ultimately show ?thesis by auto
qed

lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1"
proof -
  have "card (holdents s th - {cs}) = card (holdents s th) - 1"
  proof -
    have "cs \<in> holdents s th" using holding_th_cs_s
      by (auto simp:holdents_def)
    moreover have "finite (holdents s th)"
        by (simp add: finite_holdents) 
    ultimately show ?thesis by auto
  qed
  thus ?thesis by (unfold cntCS_def holdents_es_th)
qed

lemma holdents_kept:
  assumes "th' \<noteq> taker"
  and "th' \<noteq> th"
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
  { fix cs'
    assume h: "cs' \<in> ?L"
    have "cs' \<in> ?R"
    proof(cases "cs' = cs")
      case False
      hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
      from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
      from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
      show ?thesis
        by (unfold holdents_def s_holding_def, fold wq_def, auto)
    next
      case True
      from h[unfolded this]
      have "holding (e#s) th' cs" by (auto simp:holdents_def)
      from held_unique[OF this holding_taker]
      have "th' = taker" .
      with assms show ?thesis by auto
    qed
  } moreover {
    fix cs'
    assume h: "cs' \<in> ?R"
    have "cs' \<in> ?L"
    proof(cases "cs' = cs")
      case False
      hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
      from h have "holding s th' cs'" by (auto simp:holdents_def)
      from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
      show ?thesis
        by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
    next
      case True
      from h[unfolded this]
      have "holding s th' cs" by (auto simp:holdents_def)
      from held_unique[OF this holding_th_cs_s]
      have "th' = th" .
      with assms show ?thesis by auto
    qed
  } ultimately show ?thesis by auto
qed

lemma cntCS_kept [simp]:
  assumes "th' \<noteq> taker"
  and "th' \<noteq> th"
  shows "cntCS (e#s) th' = cntCS s th'"
  by (unfold cntCS_def holdents_kept[OF assms], simp)

lemma readys_kept1: 
  assumes "th' \<noteq> taker"
  and "th' \<in> readys (e#s)"
  shows "th' \<in> readys s"
proof -
  { fix cs'
    assume wait: "waiting s th' cs'"
    have n_wait: "\<not> waiting (e#s) th' cs'" 
        using assms(2)[unfolded readys_def] by auto
    have False
    proof(cases "cs' = cs")
      case False
      with n_wait wait
      show ?thesis 
        by (unfold s_waiting_def, fold wq_def, auto)
    next
      case True
      have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)" 
        using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] .
      moreover have "\<not> (th' \<in> set rest \<and> th' \<noteq> hd (taker # rest'))" 
        using n_wait[unfolded True s_waiting_def, folded wq_def, 
                    unfolded wq_es_cs set_wq', unfolded eq_wq'] .
      ultimately have "th' = taker" by auto
      with assms(1)
      show ?thesis by simp
    qed
  } with assms(2) show ?thesis  
    by (unfold readys_def, auto)
qed

lemma readys_kept2: 
  assumes "th' \<noteq> taker"
  and "th' \<in> readys s"
  shows "th' \<in> readys (e#s)"
proof -
  { fix cs'
    assume wait: "waiting (e#s) th' cs'"
    have n_wait: "\<not> waiting s th' cs'" 
        using assms(2)[unfolded readys_def] by auto
    have False
    proof(cases "cs' = cs")
      case False
      with n_wait wait
      show ?thesis 
        by (unfold s_waiting_def, fold wq_def, auto)
    next
      case True
      have "th' \<in> set rest \<and> th' \<noteq> hd (taker # rest')"
          using  wait [unfolded True s_waiting_def, folded wq_def, 
                    unfolded wq_es_cs set_wq', unfolded eq_wq']  .
      moreover have "\<not> (th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest))"
          using n_wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] .
      ultimately have "th' = taker" by auto
      with assms(1)
      show ?thesis by simp
    qed
  } with assms(2) show ?thesis  
    by (unfold readys_def, auto)
qed

lemma readys_simp [simp]:
  assumes "th' \<noteq> taker"
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
  using readys_kept1[OF assms] readys_kept2[OF assms]
  by metis

lemma cnp_cnv_cncs_kept:
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"
proof -
  { assume eq_th': "th' = taker"
    have ?thesis
      apply (unfold eq_th' pvD_taker_es cntCS_es_taker)
      by (insert neq_taker_th assms[unfolded eq_th'], unfold is_v, simp)
  } moreover {
    assume eq_th': "th' = th"
    have ?thesis 
      apply (unfold eq_th' pvD_th_es cntCS_es_th)
      by (insert assms[unfolded eq_th'], unfold is_v, simp)
  } moreover {
    assume h: "th' \<noteq> taker" "th' \<noteq> th"
    have ?thesis using assms
      apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp)
      by (fold is_v, unfold pvD_def, simp)
  } ultimately show ?thesis by metis
qed

end

context valid_trace_v_e
begin

lemma holdents_es_th:
  "holdents (e#s) th = holdents s th - {cs}" (is "?L = ?R")
proof -
  { fix cs'
    assume "cs' \<in> ?L"
    hence "holding (e#s) th cs'" by (auto simp:holdents_def)
    hence "cs' \<in> ?R"
    proof(cases rule:holding_esE)
      case 1
      thus ?thesis by (auto simp:holdents_def)
    qed 
  } moreover {
    fix cs'
    assume "cs' \<in> ?R"
    hence "cs' \<noteq> cs" "holding s th cs'" by (auto simp:holdents_def)
    from holding_esI2[OF this]
    have "cs' \<in> ?L" by (auto simp:holdents_def)
  } ultimately show ?thesis by auto
qed

lemma cntCS_es_th [simp]: "cntCS (e#s) th = cntCS s th - 1"
proof -
  have "card (holdents s th - {cs}) = card (holdents s th) - 1"
  proof -
    have "cs \<in> holdents s th" using holding_th_cs_s
      by (auto simp:holdents_def)
    moreover have "finite (holdents s th)"
        by (simp add: finite_holdents) 
    ultimately show ?thesis by auto
  qed
  thus ?thesis by (unfold cntCS_def holdents_es_th)
qed

lemma holdents_kept:
  assumes "th' \<noteq> th"
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
  { fix cs'
    assume h: "cs' \<in> ?L"
    have "cs' \<in> ?R"
    proof(cases "cs' = cs")
      case False
      hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
      from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
      from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
      show ?thesis
        by (unfold holdents_def s_holding_def, fold wq_def, auto)
    next
      case True
      from h[unfolded this]
      have "holding (e#s) th' cs" by (auto simp:holdents_def)
      from this[unfolded s_holding_def, folded wq_def, 
            unfolded wq_es_cs nil_wq']
      show ?thesis by auto
    qed
  } moreover {
    fix cs'
    assume h: "cs' \<in> ?R"
    have "cs' \<in> ?L"
    proof(cases "cs' = cs")
      case False
      hence eq_wq: "wq (e#s) cs' = wq s cs'" by simp
      from h have "holding s th' cs'" by (auto simp:holdents_def)
      from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
      show ?thesis
        by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
    next
      case True
      from h[unfolded this]
      have "holding s th' cs" by (auto simp:holdents_def)
      from held_unique[OF this holding_th_cs_s]
      have "th' = th" .
      with assms show ?thesis by auto
    qed
  } ultimately show ?thesis by auto
qed

lemma cntCS_kept [simp]:
  assumes "th' \<noteq> th"
  shows "cntCS (e#s) th' = cntCS s th'"
  by (unfold cntCS_def holdents_kept[OF assms], simp)

lemma readys_kept1: 
  assumes "th' \<in> readys (e#s)"
  shows "th' \<in> readys s"
proof -
  { fix cs'
    assume wait: "waiting s th' cs'"
    have n_wait: "\<not> waiting (e#s) th' cs'" 
        using assms(1)[unfolded readys_def] by auto
    have False
    proof(cases "cs' = cs")
      case False
      with n_wait wait
      show ?thesis 
        by (unfold s_waiting_def, fold wq_def, auto)
    next
      case True
      have "th' \<in> set (th # rest) \<and> th' \<noteq> hd (th # rest)" 
        using wait[unfolded True s_waiting_def, folded wq_def, unfolded wq_s_cs] . 
      hence "th' \<in> set rest" by auto
      with set_wq' have "th' \<in> set wq'" by metis
      with nil_wq' show ?thesis by simp
    qed
  } thus ?thesis using assms
    by (unfold readys_def, auto)
qed

lemma readys_kept2: 
  assumes "th' \<in> readys s"
  shows "th' \<in> readys (e#s)"
proof -
  { fix cs'
    assume wait: "waiting (e#s) th' cs'"
    have n_wait: "\<not> waiting s th' cs'" 
        using assms[unfolded readys_def] by auto
    have False
    proof(cases "cs' = cs")
      case False
      with n_wait wait
      show ?thesis 
        by (unfold s_waiting_def, fold wq_def, auto)
    next
      case True
      have "th' \<in> set [] \<and> th' \<noteq> hd []"
        using wait[unfolded True s_waiting_def, folded wq_def, 
              unfolded wq_es_cs nil_wq'] .
      thus ?thesis by simp
    qed
  } with assms show ?thesis  
    by (unfold readys_def, auto)
qed

lemma readys_simp [simp]:
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
  using readys_kept1[OF assms] readys_kept2[OF assms]
  by metis

lemma cnp_cnv_cncs_kept:
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"
proof -
  {
    assume eq_th': "th' = th"
    have ?thesis 
      apply (unfold eq_th' pvD_th_es cntCS_es_th)
      by (insert assms[unfolded eq_th'], unfold is_v, simp)
  } moreover {
    assume h: "th' \<noteq> th"
    have ?thesis using assms
      apply (unfold cntCS_kept[OF h], insert h, unfold is_v, simp)
      by (fold is_v, unfold pvD_def, simp)
  } ultimately show ?thesis by metis
qed

end

context valid_trace_v
begin

lemma cnp_cnv_cncs_kept:
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"
proof(cases "rest = []")
  case True
  then interpret vt: valid_trace_v_e by (unfold_locales, simp)
  show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast 
next
  case False
  then interpret vt: valid_trace_v_n by (unfold_locales, simp)
  show ?thesis using assms using vt.cnp_cnv_cncs_kept by blast 
qed

end

context valid_trace_create
begin

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

lemma th_not_ready_s [simp]: "th \<notin> readys s"
  using th_not_live_s by (unfold readys_def, simp)

lemma th_live_es [simp]: "th \<in> threads (e#s)"
  by (unfold is_create, simp)

lemma not_waiting_th_s [simp]: "\<not> waiting s th cs'"
proof
  assume "waiting s th cs'"
  from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
  have "th \<in> set (wq s cs')" by auto
  from wq_threads[OF this] have "th \<in> threads s" .
  with th_not_live_s show False by simp
qed

lemma not_holding_th_s [simp]: "\<not> holding s th cs'"
proof
  assume "holding s th cs'"
  from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
  have "th \<in> set (wq s cs')" by auto
  from wq_threads[OF this] have "th \<in> threads s" .
  with th_not_live_s show False by simp
qed

lemma not_waiting_th_es [simp]: "\<not> waiting (e#s) th cs'"
proof
  assume "waiting (e # s) th cs'"
  from this[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
  have "th \<in> set (wq s cs')" by auto
  from wq_threads[OF this] have "th \<in> threads s" .
  with th_not_live_s show False by simp
qed

lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"
proof
  assume "holding (e # s) th cs'"
  from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
  have "th \<in> set (wq s cs')" by auto
  from wq_threads[OF this] have "th \<in> threads s" .
  with th_not_live_s show False by simp
qed

lemma ready_th_es [simp]: "th \<in> readys (e#s)"
  by (simp add:readys_def)

lemma holdents_th_s: "holdents s th = {}"
  by (unfold holdents_def, auto)

lemma holdents_th_es: "holdents (e#s) th = {}"
  by (unfold holdents_def, auto)

lemma cntCS_th_s [simp]: "cntCS s th = 0"
  by (unfold cntCS_def, simp add:holdents_th_s)

lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0"
  by (unfold cntCS_def, simp add:holdents_th_es)

lemma pvD_th_s [simp]: "pvD s th = 0"
  by (unfold pvD_def, simp)

lemma pvD_th_es [simp]: "pvD (e#s) th = 0"
  by (unfold pvD_def, simp)

lemma holdents_kept:
  assumes "th' \<noteq> th"
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
  { fix cs'
    assume h: "cs' \<in> ?L"
    hence "cs' \<in> ?R"
      by (unfold holdents_def s_holding_def, fold wq_def, 
             unfold wq_kept, auto)
  } moreover {
    fix cs'
    assume h: "cs' \<in> ?R"
    hence "cs' \<in> ?L"
      by (unfold holdents_def s_holding_def, fold wq_def, 
             unfold wq_kept, auto)
  } ultimately show ?thesis by auto
qed

lemma cntCS_kept [simp]:
  assumes "th' \<noteq> th"
  shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")
  using holdents_kept[OF assms]
  by (unfold cntCS_def, simp)

lemma readys_kept1: 
  assumes "th' \<noteq> th"
  and "th' \<in> readys (e#s)"
  shows "th' \<in> readys s"
proof -
  { fix cs'
    assume wait: "waiting s th' cs'"
    have n_wait: "\<not> waiting (e#s) th' cs'" 
      using assms by (auto simp:readys_def)
    from wait[unfolded s_waiting_def, folded wq_def]
         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
    have False by auto
  } thus ?thesis using assms
    by (unfold readys_def, auto)
qed

lemma readys_kept2: 
  assumes "th' \<noteq> th"
  and "th' \<in> readys s"
  shows "th' \<in> readys (e#s)"
proof -
  { fix cs'
    assume wait: "waiting (e#s) th' cs'"
    have n_wait: "\<not> waiting s th' cs'"
      using assms(2) by (auto simp:readys_def)
    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
         n_wait[unfolded s_waiting_def, folded wq_def]
    have False by auto
  } with assms show ?thesis  
    by (unfold readys_def, auto)
qed

lemma readys_simp [simp]:
  assumes "th' \<noteq> th"
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
  using readys_kept1[OF assms] readys_kept2[OF assms]
  by metis

lemma pvD_kept [simp]:
  assumes "th' \<noteq> th"
  shows "pvD (e#s) th' = pvD s th'"
  using assms
  by (unfold pvD_def, simp)

lemma cnp_cnv_cncs_kept:
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"
proof -
  {
    assume eq_th': "th' = th"
    have ?thesis using assms
      by (unfold eq_th', simp, unfold is_create, simp)
  } moreover {
    assume h: "th' \<noteq> th"
    hence ?thesis using assms
      by (simp, simp add:is_create)
  } ultimately show ?thesis by metis
qed

end

context valid_trace_exit
begin

lemma th_live_s [simp]: "th \<in> threads s"
proof -
  from pip_e[unfolded is_exit]
  show ?thesis
  by (cases, unfold runing_def readys_def, simp)
qed

lemma th_ready_s [simp]: "th \<in> readys s"
proof -
  from pip_e[unfolded is_exit]
  show ?thesis
  by (cases, unfold runing_def, simp)
qed

lemma th_not_live_es [simp]: "th \<notin> threads (e#s)"
  by (unfold is_exit, simp)

lemma not_holding_th_s [simp]: "\<not> holding s th cs'"
proof -
  from pip_e[unfolded is_exit]
  show ?thesis 
   by (cases, unfold holdents_def, auto)
qed

lemma cntCS_th_s [simp]: "cntCS s th = 0"
proof -
  from pip_e[unfolded is_exit]
  show ?thesis 
   by (cases, unfold cntCS_def, simp)
qed

lemma not_holding_th_es [simp]: "\<not> holding (e#s) th cs'"
proof
  assume "holding (e # s) th cs'"
  from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
  have "holding s th cs'" 
    by (unfold s_holding_def, fold wq_def, auto)
  with not_holding_th_s 
  show False by simp
qed

lemma ready_th_es [simp]: "th \<notin> readys (e#s)"
  by (simp add:readys_def)

lemma holdents_th_s: "holdents s th = {}"
  by (unfold holdents_def, auto)

lemma holdents_th_es: "holdents (e#s) th = {}"
  by (unfold holdents_def, auto)

lemma cntCS_th_es [simp]: "cntCS (e#s) th = 0"
  by (unfold cntCS_def, simp add:holdents_th_es)

lemma pvD_th_s [simp]: "pvD s th = 0"
  by (unfold pvD_def, simp)

lemma pvD_th_es [simp]: "pvD (e#s) th = 0"
  by (unfold pvD_def, simp)

lemma holdents_kept:
  assumes "th' \<noteq> th"
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
  { fix cs'
    assume h: "cs' \<in> ?L"
    hence "cs' \<in> ?R"
      by (unfold holdents_def s_holding_def, fold wq_def, 
             unfold wq_kept, auto)
  } moreover {
    fix cs'
    assume h: "cs' \<in> ?R"
    hence "cs' \<in> ?L"
      by (unfold holdents_def s_holding_def, fold wq_def, 
             unfold wq_kept, auto)
  } ultimately show ?thesis by auto
qed

lemma cntCS_kept [simp]:
  assumes "th' \<noteq> th"
  shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")
  using holdents_kept[OF assms]
  by (unfold cntCS_def, simp)

lemma readys_kept1: 
  assumes "th' \<noteq> th"
  and "th' \<in> readys (e#s)"
  shows "th' \<in> readys s"
proof -
  { fix cs'
    assume wait: "waiting s th' cs'"
    have n_wait: "\<not> waiting (e#s) th' cs'" 
      using assms by (auto simp:readys_def)
    from wait[unfolded s_waiting_def, folded wq_def]
         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
    have False by auto
  } thus ?thesis using assms
    by (unfold readys_def, auto)
qed

lemma readys_kept2: 
  assumes "th' \<noteq> th"
  and "th' \<in> readys s"
  shows "th' \<in> readys (e#s)"
proof -
  { fix cs'
    assume wait: "waiting (e#s) th' cs'"
    have n_wait: "\<not> waiting s th' cs'"
      using assms(2) by (auto simp:readys_def)
    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
         n_wait[unfolded s_waiting_def, folded wq_def]
    have False by auto
  } with assms show ?thesis  
    by (unfold readys_def, auto)
qed

lemma readys_simp [simp]:
  assumes "th' \<noteq> th"
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
  using readys_kept1[OF assms] readys_kept2[OF assms]
  by metis

lemma pvD_kept [simp]:
  assumes "th' \<noteq> th"
  shows "pvD (e#s) th' = pvD s th'"
  using assms
  by (unfold pvD_def, simp)

lemma cnp_cnv_cncs_kept:
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"
proof -
  {
    assume eq_th': "th' = th"
    have ?thesis using assms
      by (unfold eq_th', simp, unfold is_exit, simp)
  } moreover {
    assume h: "th' \<noteq> th"
    hence ?thesis using assms
      by (simp, simp add:is_exit)
  } ultimately show ?thesis by metis
qed

end

context valid_trace_set
begin

lemma th_live_s [simp]: "th \<in> threads s"
proof -
  from pip_e[unfolded is_set]
  show ?thesis
  by (cases, unfold runing_def readys_def, simp)
qed

lemma th_ready_s [simp]: "th \<in> readys s"
proof -
  from pip_e[unfolded is_set]
  show ?thesis
  by (cases, unfold runing_def, simp)
qed

lemma th_not_live_es [simp]: "th \<in> threads (e#s)"
  by (unfold is_set, simp)


lemma holdents_kept:
  shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
proof -
  { fix cs'
    assume h: "cs' \<in> ?L"
    hence "cs' \<in> ?R"
      by (unfold holdents_def s_holding_def, fold wq_def, 
             unfold wq_kept, auto)
  } moreover {
    fix cs'
    assume h: "cs' \<in> ?R"
    hence "cs' \<in> ?L"
      by (unfold holdents_def s_holding_def, fold wq_def, 
             unfold wq_kept, auto)
  } ultimately show ?thesis by auto
qed

lemma cntCS_kept [simp]:
  shows "cntCS (e#s) th' = cntCS s th'" (is "?L = ?R")
  using holdents_kept
  by (unfold cntCS_def, simp)

lemma threads_kept[simp]:
  "threads (e#s) = threads s"
  by (unfold is_set, simp)

lemma readys_kept1: 
  assumes "th' \<in> readys (e#s)"
  shows "th' \<in> readys s"
proof -
  { fix cs'
    assume wait: "waiting s th' cs'"
    have n_wait: "\<not> waiting (e#s) th' cs'" 
      using assms by (auto simp:readys_def)
    from wait[unfolded s_waiting_def, folded wq_def]
         n_wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
    have False by auto
  } moreover have "th' \<in> threads s" 
    using assms[unfolded readys_def] by auto
  ultimately show ?thesis 
    by (unfold readys_def, auto)
qed

lemma readys_kept2: 
  assumes "th' \<in> readys s"
  shows "th' \<in> readys (e#s)"
proof -
  { fix cs'
    assume wait: "waiting (e#s) th' cs'"
    have n_wait: "\<not> waiting s th' cs'"
      using assms by (auto simp:readys_def)
    from wait[unfolded s_waiting_def, folded wq_def, unfolded wq_kept]
         n_wait[unfolded s_waiting_def, folded wq_def]
    have False by auto
  } with assms show ?thesis  
    by (unfold readys_def, auto)
qed

lemma readys_simp [simp]:
  shows "(th' \<in> readys (e#s)) = (th' \<in> readys s)"
  using readys_kept1 readys_kept2
  by metis

lemma pvD_kept [simp]:
  shows "pvD (e#s) th' = pvD s th'"
  by (unfold pvD_def, simp)

lemma cnp_cnv_cncs_kept:
  assumes "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
  shows "cntP (e#s) th' = cntV (e#s) th' +  cntCS (e#s) th' + pvD (e#s) th'"
  using assms
  by (unfold is_set, simp, fold is_set, simp)

end

context valid_trace
begin

lemma cnp_cnv_cncs: "cntP s th' = cntV s th' + cntCS s th' + pvD s th'"
proof(induct rule:ind)
  case Nil
  thus ?case 
    by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def 
              s_holding_def, simp)
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_create: valid_trace_create s e th prio 
      using Create by (unfold_locales, simp)
    show ?thesis using Cons by (simp add: vt_create.cnp_cnv_cncs_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.cnp_cnv_cncs_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.cnp_cnv_cncs_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.cnp_cnv_cncs_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.cnp_cnv_cncs_kept) 
  qed
qed

end

section {* Corollaries of @{thm valid_trace.cnp_cnv_cncs} *}

context valid_trace
begin

lemma not_thread_holdents:
  assumes not_in: "th \<notin> threads s" 
  shows "holdents s th = {}"
proof -
  { fix cs
    assume "cs \<in> holdents s th"
    hence "holding s th cs" by (auto simp:holdents_def)
    from this[unfolded s_holding_def, folded wq_def]
    have "th \<in> set (wq s cs)" by auto
    with wq_threads have "th \<in> threads s" by auto
    with assms
    have False by simp
  } thus ?thesis by auto
qed

lemma not_thread_cncs:
  assumes not_in: "th \<notin> threads s" 
  shows "cntCS s th = 0"
  using not_thread_holdents[OF assms]
  by (simp add:cntCS_def)

lemma cnp_cnv_eq:
  assumes "th \<notin> threads s"
  shows "cntP s th = cntV s th"
  using assms cnp_cnv_cncs not_thread_cncs pvD_def
  by (auto)

lemma eq_pv_children:
  assumes eq_pv: "cntP s th = cntV s th"
  shows "children (RAG s) (Th th) = {}"
proof -
    from cnp_cnv_cncs and eq_pv
    have "cntCS s th = 0" 
      by (auto split:if_splits)
    from this[unfolded cntCS_def holdents_alt_def]
    have card_0: "card (the_cs ` children (RAG s) (Th th)) = 0" .
    have "finite (the_cs ` children (RAG s) (Th th))"
      by (simp add: fsbtRAGs.finite_children)
    from card_0[unfolded card_0_eq[OF this]]
    show ?thesis by auto
qed

lemma eq_pv_holdents:
  assumes eq_pv: "cntP s th = cntV s th"
  shows "holdents s th = {}"
  by (unfold holdents_alt_def eq_pv_children[OF assms], simp)

lemma eq_pv_subtree:
  assumes eq_pv: "cntP s th = cntV s th"
  shows "subtree (RAG s) (Th th) = {Th th}"
  using eq_pv_children[OF assms]
    by (unfold subtree_children, simp)

lemma count_eq_RAG_plus:
  assumes "cntP s th = cntV s th"
  shows "{th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
proof(rule ccontr)
    assume otherwise: "{th'. (Th th', Th th) \<in> (RAG s)\<^sup>+} \<noteq> {}"
    then obtain th' where "(Th th', Th th) \<in> (RAG s)^+" by auto
    from tranclD2[OF this]
    obtain z where "z \<in> children (RAG s) (Th th)" 
      by (auto simp:children_def)
    with eq_pv_children[OF assms]
    show False by simp
qed

lemma eq_pv_dependants:
  assumes eq_pv: "cntP s th = cntV s th"
  shows "dependants s th = {}"
proof -
  from count_eq_RAG_plus[OF assms, folded dependants_alt_def1]
  show ?thesis .
qed

lemma count_eq_tRAG_plus:
  assumes "cntP s th = cntV s th"
  shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
  using assms eq_pv_dependants dependants_alt_def eq_dependants by auto 

lemma count_eq_RAG_plus_Th:
  assumes "cntP s th = cntV s th"
  shows "{Th th' | th'. (Th th', Th th) \<in> (RAG s)^+} = {}"
  using count_eq_RAG_plus[OF assms] by auto

lemma count_eq_tRAG_plus_Th:
  assumes "cntP s th = cntV s th"
  shows "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
   using count_eq_tRAG_plus[OF assms] by auto

end

section {* hhh *}

lemma RAG_tRAG_transfer:
  assumes "vt s'"
  assumes "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
  and "(Cs cs, Th th'') \<in> RAG s'"
  shows "tRAG s = tRAG s' \<union> {(Th th, Th th'')}" (is "?L = ?R")
proof -
  interpret vt_s': valid_trace "s'" using assms(1)
    by (unfold_locales, simp)
  { fix n1 n2
    assume "(n1, n2) \<in> ?L"
    from this[unfolded tRAG_alt_def]
    obtain th1 th2 cs' where 
      h: "n1 = Th th1" "n2 = Th th2" 
         "(Th th1, Cs cs') \<in> RAG s"
         "(Cs cs', Th th2) \<in> RAG s" by auto
    from h(4) and assms(2) have cs_in: "(Cs cs', Th th2) \<in> RAG s'" by auto
    from h(3) and assms(2) 
    have "(Th th1, Cs cs') = (Th th, Cs cs) \<or> 
          (Th th1, Cs cs') \<in> RAG s'" by auto
    hence "(n1, n2) \<in> ?R"
    proof
      assume h1: "(Th th1, Cs cs') = (Th th, Cs cs)"
      hence eq_th1: "th1 = th" by simp
      moreover have "th2 = th''"
      proof -
        from h1 have "cs' = cs" by simp
        from assms(3) cs_in[unfolded this]
        show ?thesis using vt_s'.unique_RAG by auto 
      qed
      ultimately show ?thesis using h(1,2) by auto
    next
      assume "(Th th1, Cs cs') \<in> RAG s'"
      with cs_in have "(Th th1, Th th2) \<in> tRAG s'"
        by (unfold tRAG_alt_def, auto)
      from this[folded h(1, 2)] show ?thesis by auto
    qed
  } moreover {
    fix n1 n2
    assume "(n1, n2) \<in> ?R"
    hence "(n1, n2) \<in>tRAG s' \<or> (n1, n2) = (Th th, Th th'')" by auto
    hence "(n1, n2) \<in> ?L" 
    proof
      assume "(n1, n2) \<in> tRAG s'"
      moreover have "... \<subseteq> ?L"
      proof(rule tRAG_mono)
        show "RAG s' \<subseteq> RAG s" by (unfold assms(2), auto)
      qed
      ultimately show ?thesis by auto
    next
      assume eq_n: "(n1, n2) = (Th th, Th th'')"
      from assms(2, 3) have "(Cs cs, Th th'') \<in> RAG s" by auto
      moreover have "(Th th, Cs cs) \<in> RAG s" using assms(2) by auto
      ultimately show ?thesis 
        by (unfold eq_n tRAG_alt_def, auto)
    qed
  } ultimately show ?thesis by auto
qed

context valid_trace
begin

lemmas RAG_tRAG_transfer = RAG_tRAG_transfer[OF vt]

end

lemma cp_alt_def1: 
  "cp s th = Max ((the_preced s o the_thread) ` (subtree (tRAG s) (Th th)))"
proof -
  have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
       ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
       by auto
  thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
qed

lemma cp_gen_def_cond: 
  assumes "x = Th th"
  shows "cp s th = cp_gen s (Th th)"
by (unfold cp_alt_def1 cp_gen_def, simp)

lemma cp_gen_over_set:
  assumes "\<forall> x \<in> A. \<exists> th. x = Th th"
  shows "cp_gen s ` A = (cp s \<circ> the_thread) ` A"
proof(rule f_image_eq)
  fix a
  assume "a \<in> A"
  from assms[rule_format, OF this]
  obtain th where eq_a: "a = Th th" by auto
  show "cp_gen s a = (cp s \<circ> the_thread) a"
    by  (unfold eq_a, simp, unfold cp_gen_def_cond[OF refl[of "Th th"]], simp)
qed

context valid_trace
begin

lemma subtree_tRAG_thread:
  assumes "th \<in> threads s"
  shows "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" (is "?L \<subseteq> ?R")
proof -
  have "?L = {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
    by (unfold tRAG_subtree_eq, simp)
  also have "... \<subseteq> ?R"
  proof
    fix x
    assume "x \<in> {Th th' |th'. Th th' \<in> subtree (RAG s) (Th th)}"
    then obtain th' where h: "x = Th th'" "Th th' \<in> subtree (RAG s) (Th th)" by auto
    from this(2)
    show "x \<in> ?R"
    proof(cases rule:subtreeE)
      case 1
      thus ?thesis by (simp add: assms h(1)) 
    next
      case 2
      thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 
    qed
  qed
  finally show ?thesis .
qed

lemma readys_root:
  assumes "th \<in> readys s"
  shows "root (RAG s) (Th th)"
proof -
  { fix x
    assume "x \<in> ancestors (RAG s) (Th th)"
    hence h: "(Th th, x) \<in> (RAG s)^+" by (auto simp:ancestors_def)
    from tranclD[OF this]
    obtain z where "(Th th, z) \<in> RAG s" by auto
    with assms(1) have False
         apply (case_tac z, auto simp:readys_def s_RAG_def s_waiting_def cs_waiting_def)
         by (fold wq_def, blast)
  } thus ?thesis by (unfold root_def, auto)
qed

lemma readys_in_no_subtree:
  assumes "th \<in> readys s"
  and "th' \<noteq> th"
  shows "Th th \<notin> subtree (RAG s) (Th th')" 
proof
   assume "Th th \<in> subtree (RAG s) (Th th')"
   thus False
   proof(cases rule:subtreeE)
      case 1
      with assms show ?thesis by auto
   next
      case 2
      with readys_root[OF assms(1)]
      show ?thesis by (auto simp:root_def)
   qed
qed

lemma not_in_thread_isolated:
  assumes "th \<notin> threads s"
  shows "(Th th) \<notin> Field (RAG s)"
proof
  assume "(Th th) \<in> Field (RAG s)"
  with dm_RAG_threads and rg_RAG_threads assms
  show False by (unfold Field_def, blast)
qed

end

definition detached :: "state \<Rightarrow> thread \<Rightarrow> bool"
  where "detached s th \<equiv> (\<not>(\<exists> cs. holding s th cs)) \<and> (\<not>(\<exists>cs. waiting s th cs))"


lemma detached_test:
  shows "detached s th = (Th th \<notin> Field (RAG s))"
apply(simp add: detached_def Field_def)
apply(simp add: s_RAG_def)
apply(simp add: s_holding_abv s_waiting_abv)
apply(simp add: Domain_iff Range_iff)
apply(simp add: wq_def)
apply(auto)
done

context valid_trace
begin

lemma detached_intro:
  assumes eq_pv: "cntP s th = cntV s th"
  shows "detached s th"
proof -
  from eq_pv cnp_cnv_cncs
  have "th \<in> readys s \<or> th \<notin> threads s" by (auto simp:pvD_def)
  thus ?thesis
  proof
    assume "th \<notin> threads s"
    with rg_RAG_threads dm_RAG_threads
    show ?thesis
      by (auto simp add: detached_def s_RAG_def s_waiting_abv 
              s_holding_abv wq_def Domain_iff Range_iff)
  next
    assume "th \<in> readys s"
    moreover have "Th th \<notin> Range (RAG s)"
    proof -
      from eq_pv_children[OF assms]
      have "children (RAG s) (Th th) = {}" .
      thus ?thesis
      by (unfold children_def, auto)
    qed
    ultimately show ?thesis
      by (auto simp add: detached_def s_RAG_def s_waiting_abv 
              s_holding_abv wq_def readys_def)
  qed
qed

lemma detached_elim:
  assumes dtc: "detached s th"
  shows "cntP s th = cntV s th"
proof -
  have cncs_z: "cntCS s th = 0"
  proof -
    from dtc have "holdents s th = {}"
      unfolding detached_def holdents_test s_RAG_def
      by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff)
    thus ?thesis by (auto simp:cntCS_def)
  qed
  show ?thesis
  proof(cases "th \<in> threads s")
    case True
    with dtc 
    have "th \<in> readys s"
      by (unfold readys_def detached_def Field_def Domain_def Range_def, 
           auto simp:waiting_eq s_RAG_def)
    with cncs_z  show ?thesis using cnp_cnv_cncs by (simp add:pvD_def)
  next
    case False
    with cncs_z and cnp_cnv_cncs show ?thesis by (simp add:pvD_def)
  qed
qed

lemma detached_eq:
  shows "(detached s th) = (cntP s th = cntV s th)"
  by (insert vt, auto intro:detached_intro detached_elim)

end

context valid_trace
begin
(* ddd *)
lemma cp_gen_rec:
  assumes "x = Th th"
  shows "cp_gen s x = Max ({the_preced s th} \<union> (cp_gen s) ` children (tRAG s) x)"
proof(cases "children (tRAG s) x = {}")
  case True
  show ?thesis
    by (unfold True cp_gen_def subtree_children, simp add:assms)
next
  case False
  hence [simp]: "children (tRAG s) x \<noteq> {}" by auto
  note fsbttRAGs.finite_subtree[simp]
  have [simp]: "finite (children (tRAG s) x)"
     by (intro rev_finite_subset[OF fsbttRAGs.finite_subtree], 
            rule children_subtree)
  { fix r x
    have "subtree r x \<noteq> {}" by (auto simp:subtree_def)
  } note this[simp]
  have [simp]: "\<exists>x\<in>children (tRAG s) x. subtree (tRAG s) x \<noteq> {}"
  proof -
    from False obtain q where "q \<in> children (tRAG s) x" by blast
    moreover have "subtree (tRAG s) q \<noteq> {}" by simp
    ultimately show ?thesis by blast
  qed
  have h: "Max ((the_preced s \<circ> the_thread) `
                ({x} \<union> \<Union>(subtree (tRAG s) ` children (tRAG s) x))) =
        Max ({the_preced s th} \<union> cp_gen s ` children (tRAG s) x)"
                     (is "?L = ?R")
  proof -
    let "Max (?f ` (?A \<union> \<Union> (?g ` ?B)))" = ?L
    let "Max (_ \<union> (?h ` ?B))" = ?R
    let ?L1 = "?f ` \<Union>(?g ` ?B)"
    have eq_Max_L1: "Max ?L1 = Max (?h ` ?B)"
    proof -
      have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp
      also have "... =  (\<Union> x \<in> ?B. ?f ` (?g x))" by auto
      finally have "Max ?L1 = Max ..." by simp
      also have "... = Max (Max ` (\<lambda>x. ?f ` subtree (tRAG s) x) ` ?B)"
        by (subst Max_UNION, simp+)
      also have "... = Max (cp_gen s ` children (tRAG s) x)"
          by (unfold image_comp cp_gen_alt_def, simp)
      finally show ?thesis .
    qed
    show ?thesis
    proof -
      have "?L = Max (?f ` ?A \<union> ?L1)" by simp
      also have "... = max (the_preced s (the_thread x)) (Max ?L1)"
            by (subst Max_Un, simp+)
      also have "... = max (?f x) (Max (?h ` ?B))"
        by (unfold eq_Max_L1, simp)
      also have "... =?R"
        by (rule max_Max_eq, (simp)+, unfold assms, simp)
      finally show ?thesis .
    qed
  qed  thus ?thesis 
          by (fold h subtree_children, unfold cp_gen_def, simp) 
qed

lemma cp_rec:
  "cp s th = Max ({the_preced s th} \<union> 
                     (cp s o the_thread) ` children (tRAG s) (Th th))"
proof -
  have "Th th = Th th" by simp
  note h =  cp_gen_def_cond[OF this] cp_gen_rec[OF this]
  show ?thesis 
  proof -
    have "cp_gen s ` children (tRAG s) (Th th) = 
                (cp s \<circ> the_thread) ` children (tRAG s) (Th th)"
    proof(rule cp_gen_over_set)
      show " \<forall>x\<in>children (tRAG s) (Th th). \<exists>th. x = Th th"
        by (unfold tRAG_alt_def, auto simp:children_def)
    qed
    thus ?thesis by (subst (1) h(1), unfold h(2), simp)
  qed
qed

lemma next_th_holding:
  assumes nxt: "next_th s th cs th'"
  shows "holding (wq s) th cs"
proof -
  from nxt[unfolded next_th_def]
  obtain rest where h: "wq s cs = th # rest"
                       "rest \<noteq> []" 
                       "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
  thus ?thesis
    by (unfold cs_holding_def, auto)
qed

lemma next_th_waiting:
  assumes nxt: "next_th s th cs th'"
  shows "waiting (wq s) th' cs"
proof -
  from nxt[unfolded next_th_def]
  obtain rest where h: "wq s cs = th # rest"
                       "rest \<noteq> []" 
                       "th' = hd (SOME q. distinct q \<and> set q = set rest)" by auto
  from wq_distinct[of cs, unfolded h]
  have dst: "distinct (th # rest)" .
  have in_rest: "th' \<in> set rest"
  proof(unfold h, rule someI2)
    show "distinct rest \<and> set rest = set rest" using dst by auto
  next
    fix x assume "distinct x \<and> set x = set rest"
    with h(2)
    show "hd x \<in> set (rest)" by (cases x, auto)
  qed
  hence "th' \<in> set (wq s cs)" by (unfold h(1), auto)
  moreover have "th' \<noteq> hd (wq s cs)"
    by (unfold h(1), insert in_rest dst, auto)
  ultimately show ?thesis by (auto simp:cs_waiting_def)
qed

lemma next_th_RAG:
  assumes nxt: "next_th (s::event list) th cs th'"
  shows "{(Cs cs, Th th), (Th th', Cs cs)} \<subseteq> RAG s"
  using vt assms next_th_holding next_th_waiting
  by (unfold s_RAG_def, simp)

end

lemma next_th_unique: 
  assumes nt1: "next_th s th cs th1"
  and nt2: "next_th s th cs th2"
  shows "th1 = th2"
using assms by (unfold next_th_def, auto)

context valid_trace
begin

lemma threads_alt_def:
  "(threads s) = (\<Union> th \<in> readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)})"
    (is "?L = ?R")
proof -
  { fix th1
    assume "th1 \<in> ?L"
    from th_chain_to_ready[OF this]
    have "th1 \<in> readys s \<or> (\<exists>th'. th' \<in> readys s \<and> (Th th1, Th th') \<in> (RAG s)\<^sup>+)" .
    hence "th1 \<in> ?R" by (auto simp:subtree_def)
  } moreover 
  { fix th'
    assume "th' \<in> ?R"
    then obtain th where h: "th \<in> readys s" " Th th' \<in> subtree (RAG s) (Th th)"
      by auto
    from this(2)
    have "th' \<in> ?L" 
    proof(cases rule:subtreeE)
      case 1
      with h(1) show ?thesis by (auto simp:readys_def)
    next
      case 2
      from tranclD[OF this(2)[unfolded ancestors_def, simplified]]
      have "Th th' \<in> Domain (RAG s)" by auto
      from dm_RAG_threads[OF this]
      show ?thesis .
    qed
  } ultimately show ?thesis by auto
qed


text {* (* ccc *) \noindent
  Since the current precedence of the threads in ready queue will always be boosted,
  there must be one inside it has the maximum precedence of the whole system. 
*}
lemma max_cp_readys_threads:
  shows "Max (cp s ` readys s) = Max (cp s ` threads s)" (is "?L = ?R")
proof(cases "readys s = {}")
  case False
  have "?R = Max (the_preced s ` threads s)" by (unfold max_cp_eq, simp)
  also have "... = 
    Max (the_preced s ` (\<Union>th\<in>readys s. {th'. Th th' \<in> subtree (RAG s) (Th th)}))" 
         by (unfold threads_alt_def, simp)
  also have "... = 
    Max ((\<Union>th\<in>readys s. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}))"
          by (unfold image_UN, simp)
  also have "... = 
    Max (Max ` (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)}) ` readys s)" 
  proof(rule Max_UNION)
    show "\<forall>M\<in>(\<lambda>x. the_preced s ` 
                    {th'. Th th' \<in> subtree (RAG s) (Th x)}) ` readys s. finite M"
                        using finite_subtree_threads by auto
  qed (auto simp:False subtree_def)
  also have "... =  
    Max ((Max \<circ> (\<lambda>th. the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})) ` readys s)" 
      by (unfold image_comp, simp)
  also have "... = ?L" (is "Max (?f ` ?A) = Max (?g ` ?A)")
  proof -
    have "(?f ` ?A) = (?g ` ?A)"
    proof(rule f_image_eq)
      fix th1 
      assume "th1 \<in> ?A"
      thus "?f th1 = ?g th1"
        by (unfold cp_alt_def, simp)
    qed
    thus ?thesis by simp
  qed
  finally show ?thesis by simp
qed (auto simp:threads_alt_def)

lemma create_pre:
  assumes stp: "step s e"
  and not_in: "th \<notin> threads s"
  and is_in: "th \<in> threads (e#s)"
  obtains prio where "e = Create th prio"
proof -
  from assms  
  show ?thesis
  proof(cases)
    case (thread_create thread prio)
    with is_in not_in have "e = Create th prio" by simp
    from that[OF this] show ?thesis .
  next
    case (thread_exit thread)
    with assms show ?thesis by (auto intro!:that)
  next
    case (thread_P thread)
    with assms show ?thesis by (auto intro!:that)
  next
    case (thread_V thread)
    with assms show ?thesis by (auto intro!:that)
  next 
    case (thread_set thread)
    with assms show ?thesis by (auto intro!:that)
  qed
qed

end

section {* Pending properties *}

lemma holding_next_thI:
  assumes "holding s th cs"
  and "length (wq s cs) > 1"
  obtains th' where "next_th s th cs th'"
proof -
  from assms(1)[folded holding_eq, unfolded cs_holding_def]
  have " th \<in> set (wq s cs) \<and> th = hd (wq s cs)" 
    by (unfold s_holding_def, fold wq_def, auto)
  then obtain rest where h1: "wq s cs = th#rest" 
    by (cases "wq s cs", auto)
  with assms(2) have h2: "rest \<noteq> []" by auto
  let ?th' = "hd (SOME q. distinct q \<and> set q = set rest)"
  have "next_th s th cs ?th'" using  h1(1) h2 
    by (unfold next_th_def, auto)
  from that[OF this] show ?thesis .
qed

context valid_trace_e 
begin

lemma actor_inv: 
  assumes "\<not> isCreate e"
  shows "actor e \<in> runing s"
  using pip_e assms 
  by (induct, auto)

end

end
author	zhangx
	Wed, 03 Feb 2016 12:04:03 +0800 (2016-02-03)
changeset 101	c7db2ccba18a
parent 100	3d2b59f15f26
child 102	3a801bbd2687
permissions	-rw-r--r--