section {* Generic aulxiliary lemmas *}

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

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

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)

lemma wq_kept [simp]: