section {*

  This file contains lemmas used to guide the recalculation of current precedence 

  after every system call (or system operation)

*}

begin

text {* (* ddd *)

  One beauty of our modelling is that we follow the definitional extension tradition of HOL.

  The benefit of such a concise and miniature model is that  large number of intuitively 

  obvious facts are derived as lemmas, rather than asserted as axioms.

*}

text {*

  However, the lemmas in the forthcoming several locales are no longer 

  obvious. These lemmas show how the current precedences should be recalculated 

  after every execution step (in our model, every step is represented by an event, 

  which in turn, represents a system call, or operation). Each operation is 

  treated in a separate locale.

  The complication of current precedence recalculation comes 

  because the changing of RAG needs to be taken into account, 

  in addition to the changing of precedence. 

  The reason RAG changing affects current precedence is that,

  according to the definition, current precedence 

  of a thread is the maximum of the precedences of every threads in its subtree, 

  where the notion of sub-tree in RAG is defined in RTree.thy.

  Therefore, for each operation, lemmas about the change of precedences 

  and RAG are derived first, on which lemmas about current precedence 

  recalculation are based on.

*}

section {* The @{term Set} operation *}

begin

text {* (* ddd *)

  The following two lemmas confirm that @{text "Set"}-operation

  only changes the precedence of the initiating thread (or actor)

  of the operation (or event).

*}

lemma eq_preced:

  assumes "th' \<noteq> th"

proof -

  from assms show ?thesis 

qed

lemma eq_the_preced: 

  assumes "th' \<noteq> th"

  using assms

  by (unfold the_preced_def, intro eq_preced, simp)

text {* (* ddd *)

  Th following lemma @{text "eq_cp_pre"} says that the priority change of @{text "th"}

  only affects those threads, which as @{text "Th th"} in their sub-trees.

  The proof of this lemma is simplified by using the alternative definition 

  of @{text "cp"}. 

*}

lemma eq_cp_pre:

proof -

  -- {* After unfolding using the alternative definition, elements 

        affecting the @{term "cp"}-value of threads become explicit. 

        We only need to prove the following: *}

        (is "Max (?f ` ?S1) = Max (?g ` ?S2)")

  proof -

    -- {* The base sets are equal. *}

    -- {* The function values on the base set are equal as well. *}

    moreover have "\<forall> e \<in> ?S2. ?f e = ?g e"

    proof

      fix th1

      assume "th1 \<in> ?S2"

      with nd have "th1 \<noteq> th" by (auto)

      from eq_the_preced[OF this]

    qed

    -- {* Therefore, the image of the functions are equal. *}

    ultimately have "(?f ` ?S1) = (?g ` ?S2)" by (auto intro!:f_image_eq)

    thus ?thesis by simp

  qed

  thus ?thesis by (simp add:cp_alt_def)

qed

text {*

  The following lemma shows that @{term "th"} is not in the 

  sub-tree of any other thread. 

*}

lemma th_in_no_subtree:

  assumes "th' \<noteq> th"

proof -

  show ?thesis by blast

qed

text {* 

  By combining @{thm "eq_cp_pre"} and @{thm "th_in_no_subtree"}, 

  it is obvious that the change of priority only affects the @{text "cp"}-value 

  of the initiating thread @{text "th"}.

*}

lemma eq_cp:

  assumes "th' \<noteq> th"

  by (rule eq_cp_pre[OF th_in_no_subtree[OF assms]])

end

section {* The @{term V} operation *}

text {*

  The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.

*}

begin

proof -

  show ?thesis

  by (unfold root_def, simp)

qed

proof -

 show ?thesis 

    by (unfold s_RAG_def holding_eq, auto)

qed

lemma ancestors_cs: 

proof -

  from this[unfolded ancestors_th] show ?thesis by simp

qed

end

text {*

  The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 

  which represents the case when there is another thread @{text "th'"}

  to take over the critical resource released by the initiating thread @{text "th"}.

*}

begin

lemma ancestors_th': 

proof -

  qed

  thus ?thesis using ancestors_th ancestors_cs by auto

qed

lemma RAG_s:

lemma subtree_kept: (* ddd *)

proof -

  have "subtree ?RAG' (Th th1) = ?R" 

  proof(rule subset_del_subtree_outside)

    proof -

      proof(rule subtree_refute)

          by (unfold ancestors_th, simp)

      next

        from assms show "Th th1 \<noteq> Th th" by simp

      qed

      proof(rule subtree_refute)

          by (unfold ancestors_cs, insert assms, auto)

      qed simp

      thus ?thesis by simp

     qed

  qed

  moreover have "subtree ?RAG'' (Th th1) =  subtree ?RAG' (Th th1)"

  proof(rule subtree_insert_next)

    proof(rule subtree_refute)

            (is "_ \<notin> ?R")

      proof -

          moreover have "Th th1 \<notin> ..." using ancestors_th' assms by simp

          ultimately show ?thesis by auto

      qed

    next

    qed

  qed

  ultimately show ?thesis by (unfold RAG_s, simp)

qed

lemma cp_kept:

end

begin

lemma subtree_kept:

  assumes "th1 \<noteq> th"

proof(unfold RAG_s, rule subset_del_subtree_outside)

  proof -

    proof(rule subtree_refute)

          by (unfold ancestors_th, simp)

    next

      from assms show "Th th1 \<noteq> Th th" by simp

    qed

    thus ?thesis by auto

  qed

qed

lemma cp_kept_1:

  assumes "th1 \<noteq> th"

proof -

  { fix n

    proof

      then obtain th' where "nn = Th th'"

        by (unfold s_RAG_def, auto)

      from this[unfolded s_RAG_def]

      from this[unfolded cs_waiting_def]

    qed

  } note h = this

  {  fix n

     hence "n = (Cs cs)"

     by (elim subtreeE, insert h, auto)

      by (auto simp:subtree_def)

  ultimately show ?thesis by auto 

qed

lemma subtree_th: 

  from edge_of_th

    by (unfold edges_in_def, auto simp:subtree_def)

qed

lemma cp_kept_2: 

lemma eq_cp:

  using cp_kept_1 cp_kept_2

  by (cases "th' = th", auto)

end

section {* The @{term P} operation *}

begin

lemma in_no_others_subtree:

  assumes "th' \<noteq> th"

proof

  thus False

  proof(cases rule:subtreeE)

    case 1

    with assms show ?thesis by auto

  next

    case 2

    with root_th show ?thesis by (auto simp:root_def)

  qed

qed

end

begin

lemma subtree_kept:

  assumes "th' \<noteq> th"

  from in_no_others_subtree[OF assms] 

qed

lemma cp_kept: 

  assumes "th' \<noteq> th"

proof -

        by (unfold preced_kept subtree_kept[OF assms], simp)

  thus ?thesis by (unfold cp_alt_def, simp)

qed

end

begin

lemma tRAG_s: 

lemma cp_kept:

proof -

  proof -

    proof

      thus False

      proof(rule subtreeE)

         from assms[unfolded tRAG_s ancestors_def, folded this]

         show ?thesis by auto

      next

         proof(rule ancestors_mono)

         qed 

           by (unfold tRAG_s, auto simp:ancestors_def)

                       by (auto simp:ancestors_def)

         with assms show ?thesis by auto

      qed

    qed

    from subtree_insert_next[OF this]

    from this[folded tRAG_s] show ?thesis .

  qed

  show ?thesis by (unfold cp_alt_def1 h preced_kept, simp)

qed

lemma cp_gen_update_stop: (* ddd *)

  using assms(3)

  case (1 x)

  show ?case (is "?L = ?R")

  proof -

    from tRAG_ancestorsE[OF 1(2)]

    obtain th2 where eq_x: "x = Th th2" by blast

    have "?L = 

    also have "... = 

    proof -

      proof -

        proof(unfold tRAG_s, rule children_union_kept)

            by (unfold tRAG_s, auto)

          note x_u = 1(2)

          proof

            show False

              case 1

              show ?thesis by (auto simp:ancestors_def acyclic_def)

            next

              case 2

              with x_u[unfolded eq_x]

            qed

          qed

        qed

        proof(rule f_image_eq)

          fix a

          assume a_in: "a \<in> ?A"

          from 1(2)

          show "?f a = ?g a"

             case in_ch

             show ?thesis

             proof(cases "a = u")

                case True

                from assms(2)[folded this] show ?thesis .

             next

                case False