locale valid_trace_create = valid_trace_e + 

  fixes th prio

  assumes is_create: "e = Create th prio"

locale valid_trace_exit = valid_trace_e + 

  fixes th

  assumes is_exit: "e = Exit th"

locale valid_trace_p = valid_trace_e + 

  fixes th cs

  assumes is_p: "e = P th cs"

locale valid_trace_v = valid_trace_e + 

  fixes th cs

  assumes is_v: "e = V th cs"

begin

  definition "rest = tl (wq s cs)"

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

end

locale valid_trace_v_n = valid_trace_v +

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

locale valid_trace_v_e = valid_trace_v +

  assumes rest_nil: "rest = []"

locale valid_trace_set= valid_trace_e + 

  fixes th prio

  assumes is_set: "e = Set th prio"

context valid_trace

begin

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

  assumes "PP []"

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

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

     shows "PP s"

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

  case Init

  from assms(1) show ?case .

next

  case (Step s e)

  show ?case

  proof(rule assms(2))

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

  next

    show "PP s" using Step by simp

  next

    show "PIP s e" using Step by simp

  qed

qed

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

proof(induct rule:ind)

  case Nil

  thus ?case by (simp add:vt_nil)

next

  case (Cons s e t)

  show ?case

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

    case True

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

    thus ?thesis using Cons

      by (simp add:valid_trace_def valid_trace_e_def, auto)

  next

    case False

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

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

    proof -

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

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

      show ?thesis by simp

    qed

    ultimately show ?thesis by simp

  qed

qed

lemma finite_threads:

  shows "finite (threads s)"

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

end

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

unfolding cp_def wq_def

apply(induct s rule: schs.induct)

apply(simp add: Let_def cpreced_initial)

apply(simp add: Let_def)

apply(simp add: Let_def)

apply(simp add: Let_def)

apply(subst (2) schs.simps)

apply(simp add: Let_def)

apply(subst (2) schs.simps)

apply(simp add: Let_def)

done

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

  by (unfold s_RAG_def, auto)

locale valid_moment = valid_trace + 

  fixes i :: nat

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

  by (unfold_locales, insert vt_moment, auto)

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

  by  (unfold s_waiting_def cs_waiting_def wq_def, auto)

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

  by (unfold s_holding_def wq_def cs_holding_def, simp)

lemma runing_wqE:

  assumes "th \<in> runing s"

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

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

proof -

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

    by (meson list.set_cases)

  have "th' = th"

  proof(rule ccontr)

    assume "th' \<noteq> th"

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

    with assms(2)

    have "waiting s th cs" 

      by (unfold s_waiting_def, fold wq_def, auto)

    with assms show False 

      by (unfold runing_def readys_def, auto)

  qed

  with eq_wq that show ?thesis by metis

qed

end

context valid_trace_create

begin

lemma wq_neq_simp [simp]:

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

    using assms unfolding is_create wq_def

  by (auto simp:Let_def)

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

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

  using assms by simp

end

context valid_trace_exit

begin

lemma wq_neq_simp [simp]:

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

    using assms unfolding is_exit wq_def

  by (auto simp:Let_def)

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

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

  using assms by simp

end

context valid_trace_p

begin

lemma wq_neq_simp [simp]:

  assumes "cs' \<noteq> cs"

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

    using assms unfolding is_p wq_def

  by (auto simp:Let_def)

lemma runing_th_s:

  shows "th \<in> runing s"

proof -

  from pip_e[unfolded is_p]

  show ?thesis by (cases, simp)

qed

lemma th_not_waiting: 

  "\<not> waiting s th c"

proof -

  have "th \<in> readys s"

    using runing_ready runing_th_s by blast 

  thus ?thesis

    by (unfold readys_def, auto)

qed

lemma waiting_neq_th: 

  assumes "waiting s t c"

  shows "t \<noteq> th"

  using assms using th_not_waiting by blast 

lemma th_not_in_wq: 

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

proof

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

  from runing_wqE[OF runing_th_s this]

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

  with otherwise

  have "holding s th cs"

    by (unfold s_holding_def, fold wq_def, simp)

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

    by (unfold s_RAG_def, fold holding_eq, auto)

  from pip_e[unfolded is_p]

  show False

  proof(cases)

    case (thread_P)

    with cs_th_RAG show ?thesis by auto

  qed

qed

lemma wq_es_cs: 

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

  by (unfold is_p wq_def, auto simp:Let_def)

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

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

proof(cases "cs' = cs")

  case True

  show ?thesis using True assms th_not_in_wq

    by (unfold True wq_es_cs, auto)

qed (insert assms, simp)

end

context valid_trace_v

begin

lemma wq_neq_simp [simp]:

  assumes "cs' \<noteq> cs"

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

    using assms unfolding is_v wq_def

  by (auto simp:Let_def)

lemma runing_th_s:

  shows "th \<in> runing s"

proof -

  from pip_e[unfolded is_v]

  show ?thesis by (cases, simp)

qed

lemma th_not_waiting: 

  "\<not> waiting s th c"

proof -

  have "th \<in> readys s"

    using runing_ready runing_th_s by blast 

  thus ?thesis

    by (unfold readys_def, auto)

qed

lemma waiting_neq_th: 

  assumes "waiting s t c"

  shows "t \<noteq> th"

  using assms using th_not_waiting by blast 

lemma wq_s_cs:

  "wq s cs = th#rest"

proof -

  from pip_e[unfolded is_v]

  show ?thesis

  proof(cases)

    case (thread_V)

    from this(2) show ?thesis

      by (unfold rest_def s_holding_def, fold wq_def,

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

  qed

qed

lemma wq_es_cs:

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

 using wq_s_cs[unfolded wq_def]

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

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

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

proof(cases "cs' = cs")

  case True

  show ?thesis

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

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

        using assms[unfolded True wq_s_cs] by auto

  qed simp

qed (insert assms, simp)

end

context valid_trace_set

begin

lemma wq_neq_simp [simp]:

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

    using assms unfolding is_set wq_def

  by (auto simp:Let_def)

lemma wq_distinct_kept:

  assumes "distinct (wq s cs')"

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

  using assms by simp

end

context valid_trace

begin

  interpret vt_e: valid_trace_e s e using Cons by simp

  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) 

    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