theory PIPBasics

imports PIPDefs RTree

begin

text {* (* ddd *)

  Following the HOL convention of {\em definitional extension}, we have

  given a concise and miniature model of PIP. To assure ourselves of the

  correctness of this model, we are going to derive a series of expected

  properties out of it.

  This file contains the very basic properties, useful for self-assurance,

  as well as for deriving more advance properties concerning the correctness

  and implementation of PIP. *}

section {* Generic auxiliary 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 following lemma says that 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" 

    unfolding s_holding_def by auto

  from that[OF this] show ?thesis .

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

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 running}, @{term readys}

  and @{term threads}.

*}

lemma running_ready: 

  shows "running s \<subseteq> readys s"

  unfolding running_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 running_wqE:

  assumes "th \<in> running 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 running_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 s_waiting_abv s_holding_abv]

  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"

  obtains cs where "e = P th cs"

proof(cases e)

  case (P th' pty)

  show ?thesis using that

  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"

  obtains cs' where "e = V th cs'"

proof(cases e)

  case (V th' pty)

  show ?thesis using that

  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)

text {* 

  The following three lemmas shows the shape

  of nodes in @{term tRAG}.

*}

lemma tRAG_nodeE:

  assumes "(n1, n2) \<in> tRAG s"

  obtains th1 th2 where "n1 = Th th1" "n2 = Th th2"

  using assms

  by (auto simp: tRAG_def wRAG_def hRAG_def)

lemma tRAG_ancestorsE:

  assumes "x \<in> ancestors (tRAG s) u"

  obtains th where "x = Th th"

proof -

  from assms have "(u, x) \<in> (tRAG s)^+" 

      by (unfold ancestors_def, auto)

  from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto

  then obtain th where "x = Th th"

    by (unfold tRAG_alt_def, auto)

  from that[OF this] show ?thesis .

qed

lemma subtree_nodeE:

  assumes "n \<in> subtree (tRAG s) (Th th)"

  obtains th1 where "n = Th th1"

proof -

  show ?thesis

  proof(rule subtreeE[OF assms])

    assume "n = Th th"

    from that[OF this] show ?thesis .

  next

    assume "Th th \<in> ancestors (tRAG s) n"

    hence "(n, Th th) \<in> (tRAG s)^+" by (auto simp:ancestors_def)

    hence "\<exists> th1. n = Th th1"

    proof(induct)

      case (base y)

      from tRAG_nodeE[OF this] show ?case by metis

    next

      case (step y z)

      thus ?case by auto

    qed

    with that show ?thesis by auto

  qed

qed

text {*

  The following lemmas relate @{term tRAG} with 

  @{term RAG} from different perspectives. 

*}

lemma tRAG_star_RAG: "(tRAG s)^* \<subseteq> (RAG s)^*"

proof -

  have "(wRAG s O hRAG s)^* \<subseteq> (RAG s O RAG s)^*" 

    by (rule rtrancl_mono, auto simp:RAG_split)

  also have "... \<subseteq> ((RAG s)^*)^*"

    by (rule rtrancl_mono, auto)

  also have "... = (RAG s)^*" by simp

  finally show ?thesis by (unfold tRAG_def, simp)

qed

lemma tRAG_subtree_RAG: "subtree (tRAG s) x \<subseteq> subtree (RAG s) x"

proof -

  { fix a

    assume "a \<in> subtree (tRAG s) x"

    hence "(a, x) \<in> (tRAG s)^*" by (auto simp:subtree_def)

    with tRAG_star_RAG

    have "(a, x) \<in> (RAG s)^*" by auto

    hence "a \<in> subtree (RAG s) x" by (auto simp:subtree_def)

  } thus ?thesis by auto

qed

lemma tRAG_trancl_eq:

   "{th'. (Th th', Th th)  \<in> (tRAG s)^+} = 

    {th'. (Th th', Th th)  \<in> (RAG s)^+}"

   (is "?L = ?R")

proof -

  { fix th'

    assume "th' \<in> ?L"

    hence "(Th th', Th th) \<in> (tRAG s)^+" by auto

    from tranclD[OF this]

    obtain z where h: "(Th th', z) \<in> tRAG s" "(z, Th th) \<in> (tRAG s)\<^sup>*" by auto

    from tRAG_subtree_RAG and this(2)

    have "(z, Th th) \<in> (RAG s)^*" by (meson subsetCE tRAG_star_RAG) 

    moreover from h(1) have "(Th th', z) \<in> (RAG s)^+" using tRAG_alt_def by auto 

    ultimately have "th' \<in> ?R"  by auto 

  } moreover 

  { fix th'

    assume "th' \<in> ?R"

    hence "(Th th', Th th) \<in> (RAG s)^+" by (auto)

    from plus_rpath[OF this]

    obtain xs where rp: "rpath (RAG s) (Th th') xs (Th th)" "xs \<noteq> []" by auto

    hence "(Th th', Th th) \<in> (tRAG s)^+"

    proof(induct xs arbitrary:th' th rule:length_induct)

      case (1 xs th' th)

      then obtain x1 xs1 where Cons1: "xs = x1#xs1" by (cases xs, auto)

      show ?case

      proof(cases "xs1")

        case Nil

        from 1(2)[unfolded Cons1 Nil]

        have rp: "rpath (RAG s) (Th th') [x1] (Th th)" .

        hence "(Th th', x1) \<in> (RAG s)" 

          by (cases, auto)

        then obtain cs where "x1 = Cs cs" 

              by (unfold s_RAG_def, auto)

        from rpath_nnl_lastE[OF rp[unfolded this]]

        show ?thesis by auto

      next

        case (Cons x2 xs2)

        from 1(2)[unfolded Cons1[unfolded this]]

        have rp: "rpath (RAG s) (Th th') (x1 # x2 # xs2) (Th th)" .

        from rpath_edges_on[OF this]

        have eds: "edges_on (Th th' # x1 # x2 # xs2) \<subseteq> RAG s" .

        have "(Th th', x1) \<in> edges_on (Th th' # x1 # x2 # xs2)"

            by (simp add: edges_on_unfold)

        with eds have rg1: "(Th th', x1) \<in> RAG s" by auto

        then obtain cs1 where eq_x1: "x1 = Cs cs1" by (unfold s_RAG_def, auto)

        have "(x1, x2) \<in> edges_on (Th th' # x1 # x2 # xs2)"

            by (simp add: edges_on_unfold)

        from this eds

        have rg2: "(x1, x2) \<in> RAG s" by auto

        from this[unfolded eq_x1] 

        obtain th1 where eq_x2: "x2 = Th th1" by (unfold s_RAG_def, auto)

        from rg1[unfolded eq_x1] rg2[unfolded eq_x1 eq_x2]

        have rt1: "(Th th', Th th1) \<in> tRAG s" by (unfold tRAG_alt_def, auto)