begin

text {* 

  The following two auxiliary lemmas are used to reason about @{term Max}.

*}

lemma image_Max_eqI: 

  assumes "finite B"

  and "b \<in> B"

  and "\<forall> x \<in> B. f x \<le> f b"

  shows "Max (f ` B) = f b"

  using assms

  using Max_eqI by blast 

lemma image_Max_subset:

  assumes "finite A"

  and "B \<subseteq> A"

  and "a \<in> B"

  and "Max (f ` A) = f a"

  shows "Max (f ` B) = f a"

proof(rule image_Max_eqI)

  show "finite B"

    using assms(1) assms(2) finite_subset by auto 

next

  show "a \<in> B" using assms by simp

next

  show "\<forall>x\<in>B. f x \<le> f a"

    by (metis Max_ge assms(1) assms(2) assms(4) 

            finite_imageI image_eqI subsetCE) 

qed

text {*

  The following locale @{text "highest_gen"} sets the basic context for our

  investigation: supposing thread @{text th} holds the highest @{term cp}-value

  in state @{text s}, which means the task for @{text th} is the 

  most urgent. We want to show that  

  @{text th} is treated correctly by PIP, which means

  @{text th} will not be blocked unreasonably by other less urgent

  threads. 

*}

locale highest_gen =

  fixes s th prio tm

  assumes vt_s: "vt s"

  and threads_s: "th \<in> threads s"

  and highest: "preced th s = Max ((cp s)`threads s)"

  -- {* The internal structure of @{term th}'s precedence is exposed:*}

  and preced_th: "preced th s = Prc prio tm" 

-- {* @{term s} is a valid trace, so it will inherit all results derived for

      a valid trace: *}

sublocale highest_gen < vat_s: valid_trace "s"

  by (unfold_locales, insert vt_s, simp)

context highest_gen

begin

text {*

  @{term tm} is the time when the precedence of @{term th} is set, so 

  @{term tm} must be a valid moment index into @{term s}.

*}

lemma lt_tm: "tm < length s"

  by (insert preced_tm_lt[OF threads_s preced_th], simp)

text {*

  Since @{term th} holds the highest precedence and @{text "cp"}

  is the highest precedence of all threads in the sub-tree of 

  @{text "th"} and @{text th} is among these threads, 

  its @{term cp} must equal to its precedence:

*}

lemma eq_cp_s_th: "cp s th = preced th s" (is "?L = ?R")

proof -

  have "?L \<le> ?R"

  by (unfold highest, rule Max_ge, 

        auto simp:threads_s finite_threads)

  moreover have "?R \<le> ?L"

    by (unfold vat_s.cp_rec, rule Max_ge, 

        auto simp:the_preced_def vat_s.fsbttRAGs.finite_children)

  ultimately show ?thesis by auto

qed

lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)"

  using eq_cp_s_th highest max_cp_eq the_preced_def by presburger

lemma highest_preced_thread: "preced th s = Max (the_preced s ` threads s)"

  by (fold eq_cp_s_th, unfold highest_cp_preced, simp)

lemma highest': "cp s th = Max (cp s ` threads s)"

  by (simp add: eq_cp_s_th highest)

end

locale extend_highest_gen = highest_gen + 

  fixes t 

  assumes vt_t: "vt (t@s)"

  and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"

  and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"

  and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"

sublocale extend_highest_gen < vat_t: valid_trace "t@s"

  by (unfold_locales, insert vt_t, simp)

lemma step_back_vt_app: 

  assumes vt_ts: "vt (t@s)" 

  shows "vt s"

proof -

  from vt_ts show ?thesis

  proof(induct t)

    case Nil

    from Nil show ?case by auto

  next

    case (Cons e t)

    assume ih: " vt (t @ s) \<Longrightarrow> vt s"

      and vt_et: "vt ((e # t) @ s)"

    show ?case

    proof(rule ih)

      show "vt (t @ s)"

      proof(rule step_back_vt)

        from vt_et show "vt (e # t @ s)" by simp

      qed

    qed

  qed

qed

(* locale red_extend_highest_gen = extend_highest_gen +

   fixes i::nat

*)

(*

sublocale red_extend_highest_gen <   red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)"

  apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric])

  apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp)

  by (unfold highest_gen_def, auto dest:step_back_vt_app)

*)

context extend_highest_gen

begin

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

  assumes 

    h0: "R []"

  and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e; 

                    extend_highest_gen s th prio tm t; 

                    extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"

  shows "R t"

proof -

  from vt_t extend_highest_gen_axioms show ?thesis

  proof(induct t)

    from h0 show "R []" .

  next

    case (Cons e t')

    assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"

      and vt_e: "vt ((e # t') @ s)"

      and et: "extend_highest_gen s th prio tm (e # t')"

    from vt_e and step_back_step have stp: "step (t'@s) e" by auto

    from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto

    show ?case

    proof(rule h2 [OF vt_ts stp _ _ _ ])

      show "R t'"

      proof(rule ih)

        from et show ext': "extend_highest_gen s th prio tm t'"

          by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

      next

        from vt_ts show "vt (t' @ s)" .

      qed

    next

      from et show "extend_highest_gen s th prio tm (e # t')" .

    next

      from et show ext': "extend_highest_gen s th prio tm t'"

          by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)

    qed

  qed

qed

lemma th_kept: "th \<in> threads (t @ s) \<and> 

                 preced th (t@s) = preced th s" (is "?Q t") 

proof -

  show ?thesis

  proof(induct rule:ind)

    case Nil

    from threads_s

    show ?case

      by auto

  next

    case (Cons e t)

    interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto

    interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto

    show ?case

    proof(cases e)

      case (Create thread prio)

      show ?thesis

      proof -

        from Cons and Create have "step (t@s) (Create thread prio)" by auto

        hence "th \<noteq> thread"

        proof(cases)

          case thread_create

          with Cons show ?thesis by auto

        qed

        hence "preced th ((e # t) @ s)  = preced th (t @ s)"

          by (unfold Create, auto simp:preced_def)

        moreover note Cons

        ultimately show ?thesis

          by (auto simp:Create)

      qed

    next

      case (Exit thread)

      from h_e.exit_diff and Exit

      have neq_th: "thread \<noteq> th" by auto

      with Cons

      show ?thesis

        by (unfold Exit, auto simp:preced_def)

    next

      case (P thread cs)

      with Cons

      show ?thesis 

        by (auto simp:P preced_def)

    next

      case (V thread cs)

      with Cons

      show ?thesis 

        by (auto simp:V preced_def)

    next

      case (Set thread prio')

      show ?thesis

      proof -

        from h_e.set_diff_low and Set

        have "th \<noteq> thread" by auto

        hence "preced th ((e # t) @ s)  = preced th (t @ s)"

          by (unfold Set, auto simp:preced_def)

        moreover note Cons

        ultimately show ?thesis

          by (auto simp:Set)

      qed

    qed

  qed

qed

text {*

  According to @{thm th_kept}, thread @{text "th"} has its living status

  and precedence kept along the way of @{text "t"}. The following lemma

  shows that this preserved precedence of @{text "th"} remains as the highest

  along the way of @{text "t"}.

  The proof goes by induction over @{text "t"} using the specialized

  induction rule @{thm ind}, followed by case analysis of each possible 

  operations of PIP. All cases follow the same pattern rendered by the 

  generalized introduction rule @{thm "image_Max_eqI"}. 

  The very essence is to show that precedences, no matter whether they 

  are newly introduced or modified, are always lower than the one held 

  by @{term "th"}, which by @{thm th_kept} is preserved along the way.

*}

lemma max_kept: "Max (the_preced (t @ s) ` (threads (t@s))) = preced th s"

proof(induct rule:ind)

  case Nil

  from highest_preced_thread

  show ?case by simp

next

  case (Cons e t)

    interpret h_e: extend_highest_gen _ _ _ _ "(e # t)" using Cons by auto

    interpret h_t: extend_highest_gen _ _ _ _ t using Cons by auto

  show ?case

  proof(cases e)

    case (Create thread prio')

    show ?thesis (is "Max (?f ` ?A) = ?t")

    proof -

      -- {* The following is the common pattern of each branch of the case analysis. *}

      -- {* The major part is to show that @{text "th"} holds the highest precedence: *}

      have "Max (?f ` ?A) = ?f th"

      proof(rule image_Max_eqI)

        show "finite ?A" using h_e.finite_threads by auto 

      next

        show "th \<in> ?A" using h_e.th_kept by auto 

      next

        show "\<forall>x\<in>?A. ?f x \<le> ?f th"

        proof 

          fix x

          assume "x \<in> ?A"

          hence "x = thread \<or> x \<in> threads (t@s)" by (auto simp:Create)

          thus "?f x \<le> ?f th"

          proof

            assume "x = thread"

            thus ?thesis 

              apply (simp add:Create the_preced_def preced_def, fold preced_def)

              using Create h_e.create_low h_t.th_kept lt_tm preced_leI2 

              preced_th by force

          next

            assume h: "x \<in> threads (t @ s)"

            from Cons(2)[unfolded Create] 

            have "x \<noteq> thread" using h by (cases, auto)

            hence "?f x = the_preced (t@s) x" 

              by (simp add:Create the_preced_def preced_def)

            hence "?f x \<le> Max (the_preced (t@s) ` threads (t@s))"

              by (simp add: h_t.finite_threads h)

            also have "... = ?f th"

              by (metis Cons.hyps(5) h_e.th_kept the_preced_def) 

            finally show ?thesis .

          qed

        qed

      qed

     -- {* The minor part is to show that the precedence of @{text "th"} 

           equals to preserved one, given by the foregoing lemma @{thm th_kept} *}

      also have "... = ?t" using h_e.th_kept the_preced_def by auto

      -- {* Then it follows trivially that the precedence preserved

            for @{term "th"} remains the maximum of all living threads along the way. *}

      finally show ?thesis .

    qed 

  next 

    case (Exit thread)

    show ?thesis (is "Max (?f ` ?A) = ?t")

    proof -

      have "Max (?f ` ?A) = ?f th"

      proof(rule image_Max_eqI)

        show "finite ?A" using h_e.finite_threads by auto 

      next

        show "th \<in> ?A" using h_e.th_kept by auto 

      next

        show "\<forall>x\<in>?A. ?f x \<le> ?f th"

        proof 

          fix x

          assume "x \<in> ?A"

          hence "x \<in> threads (t@s)" by (simp add: Exit) 

          hence "?f x \<le> Max (?f ` threads (t@s))" 

            by (simp add: h_t.finite_threads) 

          also have "... \<le> ?f th" 

            apply (simp add:Exit the_preced_def preced_def, fold preced_def)

            using Cons.hyps(5) h_t.th_kept the_preced_def by auto

          finally show "?f x \<le> ?f th" .

        qed

      qed

      also have "... = ?t" using h_e.th_kept the_preced_def by auto

      finally show ?thesis .

    qed 

  next

    case (P thread cs)

    with Cons

    show ?thesis by (auto simp:preced_def the_preced_def)

  next

    case (V thread cs)

    with Cons

    show ?thesis by (auto simp:preced_def the_preced_def)

  next 

    case (Set thread prio')

    show ?thesis (is "Max (?f ` ?A) = ?t")

    proof -

      have "Max (?f ` ?A) = ?f th"

      proof(rule image_Max_eqI)

        show "finite ?A" using h_e.finite_threads by auto 

      next

        show "th \<in> ?A" using h_e.th_kept by auto 

      next

        show "\<forall>x\<in>?A. ?f x \<le> ?f th"

        proof 

          fix x

          assume h: "x \<in> ?A"

          show "?f x \<le> ?f th"

          proof(cases "x = thread")

            case True

            moreover have "the_preced (Set thread prio' # t @ s) thread \<le> the_preced (t @ s) th"

            proof -

              have "the_preced (t @ s) th = Prc prio tm"  

                using h_t.th_kept preced_th by (simp add:the_preced_def)

              moreover have "prio' \<le> prio" using Set h_e.set_diff_low by auto

              ultimately show ?thesis by (insert lt_tm, auto simp:the_preced_def preced_def)

            qed

            ultimately show ?thesis

              by (unfold Set, simp add:the_preced_def preced_def)

          next

            case False

            then have "?f x  = the_preced (t@s) x"

              by (simp add:the_preced_def preced_def Set)

            also have "... \<le> Max (the_preced (t@s) ` threads (t@s))"

              using Set h h_t.finite_threads by auto 

            also have "... = ?f th" by (metis Cons.hyps(5) h_e.th_kept the_preced_def) 

            finally show ?thesis .

          qed

        qed

      qed

      also have "... = ?t" using h_e.th_kept the_preced_def by auto

      finally show ?thesis .

    qed 

  qed

qed

lemma max_preced: "preced th (t@s) = Max (the_preced (t@s) ` (threads (t@s)))"

  by (insert th_kept max_kept, auto)

text {*

  The reason behind the following lemma is that:

  Since @{term "cp"} is defined as the maximum precedence 

  of those threads contained in the sub-tree of node @{term "Th th"} 

  in @{term "RAG (t@s)"}, and all these threads are living threads, and 

  @{term "th"} is also among them, the maximum precedence of 

  them all must be the one for @{text "th"}.

*}

lemma th_cp_max_preced: 

  "cp (t@s) th = Max (the_preced (t@s) ` (threads (t@s)))" (is "?L = ?R") 

proof -

  let ?f = "the_preced (t@s)"

  have "?L = ?f th"

  proof(unfold cp_alt_def, rule image_Max_eqI)

    show "finite {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

    proof -

      have "{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)} = 

            the_thread ` {n . n \<in> subtree (RAG (t @ s)) (Th th) \<and>

                            (\<exists> th'. n = Th th')}"

      by (smt Collect_cong Setcompr_eq_image mem_Collect_eq the_thread.simps)

      moreover have "finite ..." by (simp add: vat_t.fsbtRAGs.finite_subtree) 

      ultimately show ?thesis by simp

    qed

  next

    show "th \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

      by (auto simp:subtree_def)

  next

    show "\<forall>x\<in>{th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}.

               the_preced (t @ s) x \<le> the_preced (t @ s) th"

    proof

      fix th'

      assume "th' \<in> {th'. Th th' \<in> subtree (RAG (t @ s)) (Th th)}"

      hence "Th th' \<in> subtree (RAG (t @ s)) (Th th)" by auto

      moreover have "... \<subseteq> Field (RAG (t @ s)) \<union> {Th th}"

        by (meson subtree_Field)

      ultimately have "Th th' \<in> ..." by auto

      hence "th' \<in> threads (t@s)" 

      proof

        assume "Th th' \<in> {Th th}"

        thus ?thesis using th_kept by auto 

      next

        assume "Th th' \<in> Field (RAG (t @ s))"

        thus ?thesis using vat_t.not_in_thread_isolated by blast 

      qed

      thus "the_preced (t @ s) th' \<le> the_preced (t @ s) th"

        by (metis Max_ge finite_imageI finite_threads image_eqI 

               max_kept th_kept the_preced_def)

    qed

  qed

  also have "... = ?R" by (simp add: max_preced the_preced_def) 

  finally show ?thesis .

qed

lemma th_cp_max[simp]: "Max (cp (t@s) ` threads (t@s)) = cp (t@s) th"

  using max_cp_eq th_cp_max_preced the_preced_def vt_t by presburger

lemma [simp]: "Max (cp (t@s) ` threads (t@s)) = Max (the_preced (t@s) ` threads (t@s))"

  by (simp add: th_cp_max_preced)

lemma [simp]: "Max (the_preced (t@s) ` threads (t@s)) = the_preced (t@s) th"

  using max_kept th_kept the_preced_def by auto

lemma [simp]: "the_preced (t@s) th = preced th (t@s)"

  using the_preced_def by auto

lemma [simp]: "preced th (t@s) = preced th s"

  by (simp add: th_kept)

lemma [simp]: "cp s th = preced th s"

  by (simp add: eq_cp_s_th)

lemma th_cp_preced [simp]: "cp (t@s) th = preced th s"

  by (fold max_kept, unfold th_cp_max_preced, simp)

lemma preced_less:

  assumes th'_in: "th' \<in> threads s"

  and neq_th': "th' \<noteq> th"

  shows "preced th' s < preced th s"

  using assms

by (metis Max.coboundedI finite_imageI highest not_le order.trans 

    preced_linorder rev_image_eqI threads_s vat_s.finite_threads 

    vat_s.le_cp)

section {* The `blocking thread` *}

text {* 

  The purpose of PIP is to ensure that the most 

  urgent thread @{term th} is not blocked unreasonably. 

  Therefore, a clear picture of the blocking thread is essential 

  to assure people that the purpose is fulfilled. 

  In this section, we are going to derive a series of lemmas 

  with finally give rise to a picture of the blocking thread. 

  By `blocking thread`, we mean a thread in running state but 

  different from thread @{term th}.

*}

text {*

  The following lemmas shows that the @{term cp}-value 

  of the blocking thread @{text th'} equals to the highest

  precedence in the whole system.

*}

lemma runing_preced_inversion:

  assumes runing': "th' \<in> runing (t@s)"

  shows "cp (t@s) th' = preced th s" (is "?L = ?R")

proof -

  have "?L = Max (cp (t @ s) ` readys (t @ s))" using assms

      by (unfold runing_def, auto)

  also have "\<dots> = ?R"

      by (metis th_cp_max th_cp_preced vat_t.max_cp_readys_threads) 

  finally show ?thesis .

qed

text {*

  The following lemma shows how the counters for @{term "P"} and

  @{term "V"} operations relate to the running threads in the states

  @{term s} and @{term "t @ s"}.  The lemma shows that if a thread's

  @{term "P"}-count equals its @{term "V"}-count (which means it no

  longer has any resource in its possession), it cannot be a running

  thread.

  The proof is by contraction with the assumption @{text "th' \<noteq> th"}.

  The key is the use of @{thm count_eq_dependants} to derive the

  emptiness of @{text th'}s @{term dependants}-set from the balance of

  its @{term P} and @{term V} counts.  From this, it can be shown

  @{text th'}s @{term cp}-value equals to its own precedence.

  On the other hand, since @{text th'} is running, by @{thm

  runing_preced_inversion}, its @{term cp}-value equals to the

  precedence of @{term th}.

  Combining the above two resukts we have that @{text th'} and @{term

  th} have the same precedence. By uniqueness of precedences, we have

  @{text "th' = th"}, which is in contradiction with the assumption

  @{text "th' \<noteq> th"}.