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

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

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

qed

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 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 (metis empty_iff list.exhaust list.set(1))

  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

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)

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