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

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