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

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

  shows "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" "(the_thread n1, the_thread n2) \<in> tG s"

  using assms

  by (unfold tRAG_def_tG tG_alt_def, auto)

lemma tG_tRAG: 

  assumes "(th1, th2) \<in> tG s"

  shows "(Th th1, Th th2) \<in> tRAG s"

  using assms

  by (unfold tRAG_def_tG, auto)

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

  assumes "(u, v) \<in> (map_prod f f ` R)"

  obtains u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R"

  using assms

  by auto

lemma map_prod_tranclE:

  assumes "(u, v) \<in> (map_prod f f ` R)^+"

  and "inj_on f (Field R)"

  obtains u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R^+"

proof -

  from assms(1)

  have "\<exists>u' v'. u = f u' \<and> v = f v' \<and> (u', v') \<in> R\<^sup>+"

  proof(induct rule:trancl_induct)

    case (base y)

    thus ?case by auto

  next

    case (step y z)

    then obtain u' v' where h1: "u = f u'"  "y = f v'" "(u', v') \<in> R\<^sup>+" by auto

    from map_prod_RE[OF step(2)] obtain v'' u'' 

                      where h2: "y = f v''" "z = f u''" "(v'', u'') \<in> R" by auto

    from h1 h2 have "f v' = f v''" by simp

    hence eq_v': "v' = v''"

    proof(cases rule:inj_onD[OF assms(2), consumes 1])

      case 1

      from h1(3) show ?case using trancl_subset_Field2[of R] by auto

    next

      case 2

      from h2(3) show ?case by (simp add: Domain.DomainI Field_def) 

    qed

    let ?u = "u'" and ?v = "u''"

    have "(?u, ?v) \<in> R^+" using h1(3)[unfolded eq_v'] h2(3) by auto

    with h1 h2

    show ?case by auto

  qed

  thus ?thesis using that by metis

qed

lemma map_prod_rtranclE:

  assumes "(u, v) \<in> (map_prod f f ` R)^*"

  and "inj_on f (Field R)"

  obtains (root) "u = v" 

        | (trancl) u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R^*"

proof -

  from rtranclD[OF assms(1)]

  have "u = v \<or> (\<exists>u' v'. u = f u' \<and> v = f v' \<and> (u', v') \<in> R\<^sup>*)"

  proof

    assume "u = v" thus ?thesis by auto

  next

    assume "u \<noteq> v \<and> (u, v) \<in> (map_prod f f ` R)\<^sup>+"

    hence "(u, v) \<in> (map_prod f f ` R)\<^sup>+" by auto

    thus ?thesis

     by (rule map_prod_tranclE[OF _ assms(2)], auto dest!:trancl_into_rtrancl)

  qed

  with that show ?thesis by auto

qed

lemma Field_tRAGE:

  assumes "n \<in> (Field (tRAG s))"

  obtains th where "n = Th th"

proof -

  from assms[unfolded tRAG_alt_def Field_def Domain_def Range_def]

  show ?thesis using that by auto

qed

lemma trancl_tG_tRAG:

  assumes "(th1, th2) \<in> (tG s)^+"

  shows "(Th th1, Th th2) \<in> (tRAG s)^+"

proof -

  have "inj_on the_thread (Field (tRAG s))"

    by (unfold inj_on_def Field_def tRAG_alt_def, auto)

  from map_prod_tranclE[OF assms[unfolded tG_def] this]

  obtain u' v' where h: "th1 = the_thread u'" "th2 = the_thread v'" "(u', v') \<in> (tRAG s)\<^sup>+"

    by auto

  hence "u' \<in> Domain ((tRAG s)\<^sup>+)" "v' \<in> Range ((tRAG s)\<^sup>+)" by (auto simp:Domain_def Range_def)

  from this[unfolded trancl_domain trancl_range]

  have "u' \<in> Field (tRAG s)" "v' \<in> Field (tRAG s)" 

    by (unfold Field_def, auto)

  then obtain th1' th2' where h': "u' = Th th1'" "v' = Th th2'"

    by (auto elim!:Field_tRAGE)

  with h have "th1' = th1" "th2' = th2" by (auto)

  from h(3)[unfolded h' this]

  show ?thesis by (auto simp:ancestors_def)

qed

lemma rtrancl_tG_tRAG:

  assumes "(th1, th2) \<in> (tG s)^*"

  shows "(Th th1, Th th2) \<in> (tRAG s)^*"

proof -

  from rtranclD[OF assms]