theory PIPBasics

imports PIPDefs

begin

section {* Generic aulxiliary lemmas *}

lemma rel_eqI:

  assumes "\<And> x y. (x,y) \<in> A \<Longrightarrow> (x,y) \<in> B"

  and "\<And> x y. (x,y) \<in> B \<Longrightarrow> (x, y) \<in> A"

  shows "A = B"

  using assms by auto

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

text {* The following lemma serves to proof @{text "preced_tm_lt"} *}

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

text {* The following lemma also serves to proof @{text "preced_tm_lt"} *}

lemma th_in_ne: "th \<in> threads s \<Longrightarrow> s \<noteq> []"

  by (induct s, auto)

text {* The following lemma is used in Correctness.thy *}

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)

text {*

  The follow lemma says if a resource is waited for, it must be held

  by someone else.

*}

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

text {* 

  The following four lemmas relate the @{term wq}

  and non-@{term wq} versions of @{term waiting}, @{term holding},

  @{term dependants} and @{term cp}.

*}

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 eq_dependants: "dependants (wq s) = dependants s"

  by (simp add: s_dependants_abv wq_def)

lemma cp_eq: "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

text {*

  The following lemmas is an alternative definition of @{term cp},

  which is based on the notion of subtrees in @{term RAG} and 

  is handy to use once the abstract theory of {\em relational graph}

  (and specifically {\em relational tree} and {\em relational forest})

  are in place.

*}

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_def, fold the_preced_def, simp)

qed

text {*

  The following @{text "children_RAG_alt_def"} relates

  @{term children} in @{term RAG} to the notion of @{term holding}.

  It is a technical lemmas used to prove the two following lemmas.

*}

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)

text {*

  The following two lemmas relate @{term holdents} and @{term cntCS}

  to @{term children} in @{term RAG}, so that proofs about

  @{term holdents} and @{term cntCS} can be carried out under 

  the support of the abstract theory of {\em relational graph}

  (and specifically {\em relational tree} and {\em relational forest}).

*}

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)

text {*

  The following two lemmas show the inclusion relations

  among three key sets, namely @{term runing}, @{term readys}

  and @{term threads}.

*}

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

text {*

  The following lemma says that if a thread is running, 

  it must be the head of every waiting queue it is in. 

  In other words, a running thread must have got every 

  resource it has requested.

*}

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)

text {*

  The following three lemmas establishes the uniqueness of

  precedence, a key property about precedence.

  The first two are just technical lemmas to assist the proof

  of the third.

*}

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

text {*

  The following lemma shows that there exits a linear order

  on precedences, which is crucial for the notion of 

  @{term Max} to be applicable.

*}

lemma preced_linorder: 

  assumes neq_12: "th1 \<noteq> th2"

  and th_in1: "th1 \<in> threads s"

  and th_in2: " th2 \<in> threads s"

  shows "preced th1 s < preced th2 s \<or> preced th1 s > preced th2 s"

proof -

  from preced_unique [OF _ th_in1 th_in2] and neq_12 

  have "preced th1 s \<noteq> preced th2 s" by auto

  thus ?thesis by auto

qed

text {*

  The following lemma case analysis the situations when

  two nodes are in @{term RAG}.

*}

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

text {*

  The following lemmas are the simplification rules 

  for @{term count}, @{term cntP}, @{term cntV}.

  It is part of the scheme to use the counting 

  of @{term "P"} and @{term "V"} operations to reason about

  the number of resources occupied by one thread.

*}

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

text {*

  The following two lemmas show that only @{term P}

  and @{term V} operation can change the value 

  of @{term cntP} and @{term cntV}, which is true

  obviously.

*}

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)

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