Mercurial Mercurial > hg > pip / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PIPBasics.thy
changeset 136 fb3f52fe99d1
parent 134 8a13b37b4d95
child 137 785c0f6b8184
equal deleted inserted replaced
135:9b5da0327d43 136:fb3f52fe99d1 
   374   assumes "(n1, n2) \<in> tRAG s"
 
   374   assumes "(n1, n2) \<in> tRAG s"
 
   375   obtains th1 th2 where "n1 = Th th1" "n2 = Th th2"
 
   375   obtains th1 th2 where "n1 = Th th1" "n2 = Th th2"
 
   376   using assms
 
   376   using assms
 
   377   by (auto simp: tRAG_def wRAG_def hRAG_def)
 
   377   by (auto simp: tRAG_def wRAG_def hRAG_def)
 
   378 
   378 
       
   379 lemma tRAG_tG:
 
       
   380   assumes "(n1, n2) \<in> tRAG s"
 
       
   381   shows "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" "(the_thread n1, the_thread n2) \<in> tG s"
 
       
   382   using assms
 
       
   383   by (unfold tRAG_def_tG tG_alt_def, auto)
 
       
   384 
       
   385 lemma tG_tRAG: 
       
   386   assumes "(th1, th2) \<in> tG s"
 
       
   387   shows "(Th th1, Th th2) \<in> tRAG s"
 
       
   388   using assms
 
       
   389   by (unfold tRAG_def_tG, auto)
 
       
   390 
   379 lemma tRAG_ancestorsE:
 
   391 lemma tRAG_ancestorsE:
 
   380   assumes "x \<in> ancestors (tRAG s) u"
 
   392   assumes "x \<in> ancestors (tRAG s) u"
 
   381   obtains th where "x = Th th"
 
   393   obtains th where "x = Th th"
 
   382 proof -
 
   394 proof -
 
   383   from assms have "(u, x) \<in> (tRAG s)^+" 
   395   from assms have "(u, x) \<in> (tRAG s)^+" 
   384       by (unfold ancestors_def, auto)
 
   396       by (unfold ancestors_def, auto)
 
   385   from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
 
   397   from tranclE[OF this] obtain c where "(c, x) \<in> tRAG s" by auto
 
   386   then obtain th where "x = Th th"
 
   398   then obtain th where "x = Th th"
 
   387     by (unfold tRAG_alt_def, auto)
 
   399     by (unfold tRAG_alt_def, auto)
 
   388   from that[OF this] show ?thesis .
 
   400   from that[OF this] show ?thesis .
 
       
   401 qed
 
       
   402 
       
   403 lemma map_prod_RE:
 
       
   404   assumes "(u, v) \<in> (map_prod f f ` R)"
 
       
   405   obtains u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R"
 
       
   406   using assms
 
       
   407   by auto
 
       
   408 
       
   409 lemma map_prod_tranclE:
 
       
   410   assumes "(u, v) \<in> (map_prod f f ` R)^+"
 
       
   411   and "inj_on f (Field R)"
 
       
   412   obtains u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R^+"
 
       
   413 proof -
 
       
   414   from assms(1)
 
       
   415   have "\<exists>u' v'. u = f u' \<and> v = f v' \<and> (u', v') \<in> R\<^sup>+"
 
       
   416   proof(induct rule:trancl_induct)
 
       
   417     case (base y)
 
       
   418     thus ?case by auto
 
       
   419   next
 
       
   420     case (step y z)
 
       
   421     then obtain u' v' where h1: "u = f u'"  "y = f v'" "(u', v') \<in> R\<^sup>+" by auto
 
       
   422     from map_prod_RE[OF step(2)] obtain v'' u'' 
       
   423                       where h2: "y = f v''" "z = f u''" "(v'', u'') \<in> R" by auto
 
       
   424     from h1 h2 have "f v' = f v''" by simp
 
       
   425     hence eq_v': "v' = v''"
 
       
   426     proof(cases rule:inj_onD[OF assms(2), consumes 1])
 
       
   427       case 1
 
       
   428       from h1(3) show ?case using trancl_subset_Field2[of R] by auto
 
       
   429     next
 
       
   430       case 2
 
       
   431       from h2(3) show ?case by (simp add: Domain.DomainI Field_def) 
       
   432     qed
 
       
   433     let ?u = "u'" and ?v = "u''"
 
       
   434     have "(?u, ?v) \<in> R^+" using h1(3)[unfolded eq_v'] h2(3) by auto
 
       
   435     with h1 h2
 
       
   436     show ?case by auto
 
       
   437   qed
 
       
   438   thus ?thesis using that by metis
 
       
   439 qed
 
       
   440 
       
   441 lemma map_prod_rtranclE:
 
       
   442   assumes "(u, v) \<in> (map_prod f f ` R)^*"
 
       
   443   and "inj_on f (Field R)"
 
       
   444   obtains (root) "u = v" 
       
   445         | (trancl) u' v' where "u = (f u')" "v = (f v')" "(u', v') \<in> R^*"
 
       
   446 proof -
 
       
   447   from rtranclD[OF assms(1)]
 
       
   448   have "u = v \<or> (\<exists>u' v'. u = f u' \<and> v = f v' \<and> (u', v') \<in> R\<^sup>*)"
 
       
   449   proof
 
       
   450     assume "u = v" thus ?thesis by auto
 
       
   451   next
 
       
   452     assume "u \<noteq> v \<and> (u, v) \<in> (map_prod f f ` R)\<^sup>+"
 
       
   453     hence "(u, v) \<in> (map_prod f f ` R)\<^sup>+" by auto
 
       
   454     thus ?thesis
 
       
   455      by (rule map_prod_tranclE[OF _ assms(2)], auto dest!:trancl_into_rtrancl)
 
       
   456   qed
 
       
   457   with that show ?thesis by auto
 
       
   458 qed
 
       
   459 
       
   460 lemma Field_tRAGE:
 
       
   461   assumes "n \<in> (Field (tRAG s))"
 
       
   462   obtains th where "n = Th th"
 
       
   463 proof -
 
       
   464   from assms[unfolded tRAG_alt_def Field_def Domain_def Range_def]
 
       
   465   show ?thesis using that by auto
 
       
   466 qed
 
       
   467 
       
   468 lemma trancl_tG_tRAG:
 
       
   469   assumes "(th1, th2) \<in> (tG s)^+"
 
       
   470   shows "(Th th1, Th th2) \<in> (tRAG s)^+"
 
       
   471 proof -
 
       
   472   have "inj_on the_thread (Field (tRAG s))"
 
       
   473     by (unfold inj_on_def Field_def tRAG_alt_def, auto)
 
       
   474   from map_prod_tranclE[OF assms[unfolded tG_def] this]
 
       
   475   obtain u' v' where h: "th1 = the_thread u'" "th2 = the_thread v'" "(u', v') \<in> (tRAG s)\<^sup>+"
 
       
   476     by auto
 
       
   477   hence "u' \<in> Domain ((tRAG s)\<^sup>+)" "v' \<in> Range ((tRAG s)\<^sup>+)" by (auto simp:Domain_def Range_def)
 
       
   478   from this[unfolded trancl_domain trancl_range]
 
       
   479   have "u' \<in> Field (tRAG s)" "v' \<in> Field (tRAG s)" 
       
   480     by (unfold Field_def, auto)
 
       
   481   then obtain th1' th2' where h': "u' = Th th1'" "v' = Th th2'"
 
       
   482     by (auto elim!:Field_tRAGE)
 
       
   483   with h have "th1' = th1" "th2' = th2" by (auto)
 
       
   484   from h(3)[unfolded h' this]
 
       
   485   show ?thesis by (auto simp:ancestors_def)
 
       
   486 qed
 
       
   487 
       
   488 lemma rtrancl_tG_tRAG:
 
       
   489   assumes "(th1, th2) \<in> (tG s)^*"
 
       
   490   shows "(Th th1, Th th2) \<in> (tRAG s)^*"
 
       
   491 proof -
 
       
   492   from rtranclD[OF assms]
 
       
   493   show ?thesis
 
       
   494   proof
 
       
   495     assume "th1 = th2" thus "(Th th1, Th th2) \<in> (tRAG s)\<^sup>*" by auto
 
       
   496   next
 
       
   497     assume "th1 \<noteq> th2 \<and> (th1, th2) \<in> (tG s)\<^sup>+"
 
       
   498     hence "(th1, th2) \<in> (tG s)\<^sup>+" by auto
 
       
   499     from trancl_into_rtrancl[OF trancl_tG_tRAG[OF this]]
 
       
   500     show "(Th th1, Th th2) \<in> (tRAG s)\<^sup>*" .
 
       
   501   qed
 
       
   502 qed
 
       
   503 
       
   504 lemma trancl_tRAG_tG:
 
       
   505   assumes "(n1, n2) \<in> (tRAG s)^+"
 
       
   506   obtains "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" 
       
   507           "(the_thread n1, the_thread n2) \<in> (tG s)^+"
 
       
   508 proof -
 
       
   509   have inj: "inj_on Th (Field (tG s))" 
       
   510     by (unfold inj_on_def Field_def, auto)
 
       
   511   show ?thesis 
       
   512     by (rule map_prod_tranclE[OF assms[unfolded tRAG_def_tG] inj], auto intro!:that)
 
       
   513 qed
 
       
   514 
       
   515 lemma rtrancl_tRAG_tG:
 
       
   516   assumes "(n1, n2) \<in> (tRAG s)^*"
 
       
   517   obtains "n1 = n2" 
       
   518           | "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" "the_thread n1 \<noteq> the_thread n2"
 
       
   519             "(the_thread n1, the_thread n2) \<in> (tG s)^*"
 
       
   520 proof -
 
       
   521   from rtranclD[OF assms]
 
       
   522   have "n1 = n2 \<or>
 
       
   523           n1 = Th (the_thread n1) \<and> n2 = Th (the_thread n2) \<and> the_thread n1 \<noteq> the_thread n2 \<and>
 
       
   524           (the_thread n1, the_thread n2) \<in> (tG s)^*"
 
       
   525   proof
 
       
   526     assume h: "n1 \<noteq> n2 \<and> (n1, n2) \<in> (tRAG s)\<^sup>+"
 
       
   527     hence "(n1, n2) \<in> (tRAG s)\<^sup>+" by auto
 
       
   528     from trancl_tRAG_tG[OF this]
 
       
   529     have "n1 = Th (the_thread n1)" "n2 = Th (the_thread n2)" 
       
   530           "(the_thread n1, the_thread n2) \<in> (tG s)\<^sup>+" by auto
 
       
   531     with h 
       
   532     show ?thesis by auto
 
       
   533   qed auto
 
       
   534     with that show ?thesis by auto
 
       
   535 qed
 
       
   536 
       
   537 lemma ancestors_imageE:
 
       
   538   assumes "u \<in> ancestors ((map_prod f f) ` R) v"
 
       
   539   and "inj_on f (Field R)"
 
       
   540   obtains u' v' where "u = (f u')" "v = (f v')" "u' \<in> ancestors R v'"
 
       
   541   using assms unfolding ancestors_def
 
       
   542   by (metis map_prod_tranclE mem_Collect_eq)
 
       
   543 
       
   544 lemma tRAG_ancestorsE_tG:
 
       
   545   assumes "x \<in> ancestors (tRAG s) u"
 
       
   546   obtains "x = Th (the_thread x)" "u = Th (the_thread u)" 
       
   547            "the_thread x \<in> ancestors (tG s) (the_thread u)"
 
       
   548 proof -
 
       
   549   from assms[unfolded ancestors_def]
 
       
   550   have "(u, x) \<in> (tRAG s)\<^sup>+" by simp
 
       
   551   from trancl_tRAG_tG[OF this]
 
       
   552   show ?thesis using that by (auto simp:ancestors_def)
 
       
   553 qed
 
       
   554 
       
   555 lemma ancestors_tG_tRAG:
 
       
   556   assumes "th1 \<in> ancestors (tG s) th2"
 
       
   557   shows "Th th1 \<in> ancestors (tRAG s) (Th th2)"
 
       
   558 proof -
 
       
   559   from assms[unfolded ancestors_def]
 
       
   560   have "(th2, th1) \<in> (tG s)\<^sup>+" by simp
 
       
   561   from trancl_tG_tRAG[OF this]
 
       
   562   show ?thesis by (simp add:ancestors_def)
 
   389 qed
 
   563 qed
 
   390 
   564 
   391 lemma subtree_nodeE:
 
   565 lemma subtree_nodeE:
 
   392   assumes "n \<in> subtree (tRAG s) (Th th)"
 
   566   assumes "n \<in> subtree (tRAG s) (Th th)"
 
   393   obtains th1 where "n = Th th1"
 
   567   obtains th1 where "n = Th th1"
 
   407       case (step y z)
 
   581       case (step y z)
 
   408       thus ?case by auto
 
   582       thus ?case by auto
 
   409     qed
 
   583     qed
 
   410     with that show ?thesis by auto
 
   584     with that show ?thesis by auto
 
   411   qed
 
   585   qed
 
       
   586 qed
 
       
   587 
       
   588 lemma subtree_nodeE_tG:
 
       
   589   assumes "n \<in> subtree (tRAG s) (Th th)"
 
       
   590   obtains "n = Th (the_thread n)" "the_thread n \<in> subtree (tG s) th" 
       
   591 proof -
 
       
   592   from assms[unfolded subtree_def]
 
       
   593   have "(n, Th th) \<in> (tRAG s)\<^sup>*" by simp
 
       
   594   hence "n = Th (the_thread n) \<and> the_thread n \<in> subtree (tG s) th"
 
       
   595    by (cases rule:rtrancl_tRAG_tG, auto simp:subtree_def)
 
       
   596   thus ?thesis using that by auto
 
       
   597 qed
 
       
   598 
       
   599 lemma subtree_tRAG_tG:
 
       
   600   "subtree (tRAG s) (Th th) = Th ` (subtree (tG s) th)" (is "?L = ?R")
 
       
   601 proof -
 
       
   602   { fix n
 
       
   603     assume "n \<in> ?L"
 
       
   604     from subtree_nodeE_tG[OF this]
 
       
   605     have "n \<in> ?R" by auto
 
       
   606   } moreover {
 
       
   607     fix n
 
       
   608     assume "n \<in> ?R"
 
       
   609     then obtain th' where h: "th' \<in> subtree (tG s) th" "n = Th th'" by auto
 
       
   610     hence "(th', th) \<in> (tG s)^*" by (auto simp:subtree_def)
 
       
   611     from rtrancl_tG_tRAG[OF this] and h
 
       
   612     have "n \<in> ?L" by (auto simp:subtree_def)
 
       
   613   } ultimately show ?thesis by auto
 
       
   614 qed
 
       
   615 
       
   616 lemma subtree_tG_tRAG:
 
       
   617   "(subtree (tG s) th) = the_thread ` (subtree (tRAG s) (Th th))" (is "?L = ?R")
 
       
   618 proof -
 
       
   619   have "?R = (the_thread \<circ> Th) ` subtree (tG s) th"
 
       
   620     by (unfold subtree_tRAG_tG image_comp, simp)
 
       
   621   also have "... = id ` ?L" by (rule image_cong, auto)
 
       
   622   finally show ?thesis by simp
 
   412 qed
 
   623 qed
 
   413 
   624 
   414 text {*
 
   625 text {*
 
   415   The following lemmas relate @{term tRAG} with 
   626   The following lemmas relate @{term tRAG} with 
   416   @{term RAG} from different perspectives. 
   627   @{term RAG} from different perspectives. 
   509     qed
 
   720     qed
 
   510     hence "th' \<in> ?L" by auto
 
   721     hence "th' \<in> ?L" by auto
 
   511   } ultimately show ?thesis by blast
 
   722   } ultimately show ?thesis by blast
 
   512 qed
 
   723 qed
 
   513 
   724 
   514 (*
 
       
   515 lemma image_eq:
 
       
   516   assumes "A = B"
 
       
   517   shows "f ` A = f ` B"
 
       
   518   using assms by auto
 
       
   519 *)
 
       
   520 
   725 
   521 lemma tRAG_trancl_eq_Th:
 
   726 lemma tRAG_trancl_eq_Th:
 
   522    "{Th th' | th'. (Th th', Th th)  \<in> (tRAG s)^+} = 
   727    "{Th th' | th'. (Th th', Th th)  \<in> (tRAG s)^+} = 
   523     {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}"
 
   728     {Th th' | th'. (Th th', Th th)  \<in> (RAG s)^+}"
 
   524     using tRAG_trancl_eq by auto
 
   729     using tRAG_trancl_eq by auto
 
   530 lemma tRAG_mono:
 
   735 lemma tRAG_mono:
 
   531   assumes "RAG s' \<subseteq> RAG s"
 
   736   assumes "RAG s' \<subseteq> RAG s"
 
   532   shows "tRAG s' \<subseteq> tRAG s"
 
   737   shows "tRAG s' \<subseteq> tRAG s"
 
   533   using assms 
   738   using assms 
   534   by (unfold tRAG_alt_def, auto)
 
   739   by (unfold tRAG_alt_def, auto)
 
       
   740 
   535 
   741 
   536 lemma tRAG_subtree_eq: 
   742 lemma tRAG_subtree_eq: 
   537    "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th'  \<in> (subtree (RAG s) (Th th))}"
 
   743    "(subtree (tRAG s) (Th th)) = {Th th' | th'. Th th'  \<in> (subtree (RAG s) (Th th))}"
 
   538    (is "?L = ?R")
 
   744    (is "?L = ?R")
 
   539 proof -
 
   745 proof -
 
   597   have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
 
   803   have "(the_preced s ` the_thread ` subtree (tRAG s) (Th th)) =
 
   598        ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
 
   804        ((the_preced s \<circ> the_thread) ` subtree (tRAG s) (Th th))"
 
   599        by auto
 
   805        by auto
 
   600   thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
 
   806   thus ?thesis by (unfold cp_alt_def, fold threads_set_eq, auto)
 
   601 qed
 
   807 qed
 
       
   808 
       
   809 text {*
 
       
   810   The following is another definition of @{term cp} based on @{term tG}:
 
       
   811 *}
 
       
   812 lemma cp_alt_def2: 
       
   813   "cp s th = Max (the_preced s ` (subtree (tG s) th))"
 
       
   814   by (unfold cp_alt_def1 subtree_tG_tRAG image_comp, simp)
 
       
   815 
   602 
   816 
   603 lemma RAG_tRAG_transfer:
 
   817 lemma RAG_tRAG_transfer:
 
   604   assumes  "RAG s' = RAG s \<union> {(Th th, Cs cs)}"
 
   818   assumes  "RAG s' = RAG s \<union> {(Th th, Cs cs)}"
 
   605   and "(Cs cs, Th th'') \<in> RAG s"
 
   819   and "(Cs cs, Th th'') \<in> RAG s"
 
   606   shows "tRAG s' = tRAG s \<union> {(Th th, Th th'')}" (is "?L = ?R")
 
   820   shows "tRAG s' = tRAG s \<union> {(Th th, Th th'')}" (is "?L = ?R")
 
   673 *}
 
   887 *}
 
   674 
   888 
   675 lemma dependants_alt_def1:
 
   889 lemma dependants_alt_def1:
 
   676   "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"
 
   890   "dependants (s::state) th = {th'. (Th th', Th th) \<in> (RAG s)^+}"
 
   677   using dependants_alt_def tRAG_trancl_eq by auto
 
   891   using dependants_alt_def tRAG_trancl_eq by auto
 
       
   892 
       
   893 text {*
 
       
   894   Another definition of dependants based on @{term tG}:
 
       
   895 *}
 
       
   896 lemma dependants_alt_tG:
 
       
   897   "dependants s th = {th'. (th', th) \<in> (tG s)^+}" (is "?L = ?R")
 
       
   898 proof -
 
       
   899   have "?L = {th'. (Th th', Th th) \<in> (tRAG s)\<^sup>+}"
 
       
   900     by (unfold dependants_alt_def, simp)
 
       
   901   also have "... = ?R" (is "?LL = ?RR")
 
       
   902   proof -
 
       
   903     { fix th'
 
       
   904       assume "th' \<in> ?LL"
 
       
   905       hence "(Th th', Th th) \<in> (tRAG s)\<^sup>+" by simp
 
       
   906       from trancl_tRAG_tG[OF this]
 
       
   907       have "th' \<in> ?RR" by auto
 
       
   908     } moreover {
 
       
   909       fix th'
 
       
   910       assume "th' \<in> ?RR"
 
       
   911       hence "(th', th) \<in> (tG s)\<^sup>+" by simp
 
       
   912       from trancl_tG_tRAG[OF this]
 
       
   913       have "th' \<in> ?LL" by auto
 
       
   914     } ultimately show ?thesis by auto
 
       
   915   qed
 
       
   916   finally show ?thesis .
 
       
   917 qed
 
       
   918 
       
   919 lemma dependants_alt_def_tG_ancestors:
 
       
   920   "dependants s th =  {th'. th \<in> ancestors (tG s) th'}"
 
       
   921   by (unfold dependants_alt_tG ancestors_def, simp)
 
   678 
   922 
   679 section {* Locales used to investigate the execution of PIP *}
 
   923 section {* Locales used to investigate the execution of PIP *}
 
   680 
   924 
   681 text {* 
   925 text {* 
   682   The following locale @{text valid_trace} is used to constrain the 
   926   The following locale @{text valid_trace} is used to constrain the 
  1393   then have "th \<in> set (wq s cs)"
 
  1637   then have "th \<in> set (wq s cs)"
 
  1394     using in_RAG_E s_waiting_def wq_def by auto
 
  1638     using in_RAG_E s_waiting_def wq_def by auto
 
  1395   then show ?thesis using wq_threads by simp
 
  1639   then show ?thesis using wq_threads by simp
 
  1396 qed
 
  1640 qed
 
  1397 
  1641 
       
  1642 lemma dm_tG_threads: 
       
  1643   assumes "th \<in> Domain (tG s)"
 
       
  1644   shows "th \<in> threads s"
 
       
  1645 proof -
 
       
  1646   from assms[unfolded tG_alt_def]
 
       
  1647   have "(Th th) \<in> Domain (RAG s)" by (unfold Domain_def, auto)
 
       
  1648   from dm_RAG_threads[OF this] show ?thesis .
 
       
  1649 qed
 
       
  1650 
  1398 lemma rg_RAG_threads: 
  1651 lemma rg_RAG_threads: 
  1399   assumes "(Th th) \<in> Range (RAG s)"
 
  1652   assumes "(Th th) \<in> Range (RAG s)"
 
  1400   shows "th \<in> threads s"
 
  1653   shows "th \<in> threads s"
 
  1401   using assms
 
  1654   using assms
 
  1402   apply(erule_tac RangeE)
 
  1655   apply(erule_tac RangeE)
 
  1403   apply(erule_tac in_RAG_E)
 
  1656   apply(erule_tac in_RAG_E)
 
  1404   apply(auto)
 
  1657   apply(auto)
 
  1405   using s_holding_def wq_def wq_threads by auto
 
  1658   using s_holding_def wq_def wq_threads by auto
 
  1406 
  1659 
       
  1660 lemma rg_tG_threads: 
       
  1661   assumes "th \<in> Range (tG s)"
 
       
  1662   shows "th \<in> threads s"
 
       
  1663 proof -
 
       
  1664   from assms[unfolded tG_alt_def]
 
       
  1665   have "(Th th) \<in> Range (RAG s)" by (unfold Range_def, auto)
 
       
  1666   from rg_RAG_threads[OF this] show ?thesis .
 
       
  1667 qed
 
       
  1668 
  1407 lemma RAG_threads:
 
  1669 lemma RAG_threads:
 
  1408   assumes "(Th th) \<in> Field (RAG s)"
 
  1670   assumes "(Th th) \<in> Field (RAG s)"
 
  1409   shows "th \<in> threads s"
 
  1671   shows "th \<in> threads s"
 
  1410   using assms
 
  1672   using assms
 
  1411   by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)
 
  1673   by (metis Field_def UnE dm_RAG_threads rg_RAG_threads)
 
  1412 
  1674 
       
  1675 lemma tG_threads:
 
       
  1676   assumes "th \<in> Field (tG s)"
 
       
  1677   shows "th \<in> threads s"
 
       
  1678   using assms
 
       
  1679   by (metis Field_def UnE dm_tG_threads rg_tG_threads)
 
       
  1680 
  1413 lemma not_in_thread_isolated:
 
  1681 lemma not_in_thread_isolated:
 
  1414   assumes "th \<notin> threads s"
 
  1682   assumes "th \<notin> threads s"
 
  1415   shows "(Th th) \<notin> Field (RAG s)"
 
  1683   shows "(Th th) \<notin> Field (RAG s)"
 
  1416   using RAG_threads assms by auto
 
  1684   using RAG_threads assms by auto
 
       
  1685 
       
  1686 lemma not_in_thread_isolated_tG:
 
       
  1687   assumes "th \<notin> threads s"
 
       
  1688   shows "th \<notin> Field (tG s)"
 
       
  1689   using assms
 
       
  1690   using tG_threads by auto
 
  1417 
  1691 
  1418 text {*
 
  1692 text {*
 
  1419   As a corollary, this lemma shows that @{term tRAG}
 
  1693   As a corollary, this lemma shows that @{term tRAG}
 
  1420   is also covered by the @{term threads}-set.
 
  1694   is also covered by the @{term threads}-set.
 
  1421 *}
 
  1695 *}
 
  1439       case 2
 
  1713       case 2
 
  1440       thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 
  1714       thus ?thesis by (metis ancestors_Field dm_RAG_threads h(1) image_eqI) 
  1441     qed
 
  1715     qed
 
  1442   qed
 
  1716   qed
 
  1443   finally show ?thesis .
 
  1717   finally show ?thesis .
 
       
  1718 qed
 
       
  1719 
       
  1720 lemma subtree_tG_thread:
 
       
  1721   assumes "th \<in> threads s"
 
       
  1722   shows "subtree (tG s) th \<subseteq> threads s" (is "?L \<subseteq> ?R")
 
       
  1723 proof -
 
       
  1724   from subtree_tRAG_thread[OF assms]
 
       
  1725   have "subtree (tRAG s) (Th th) \<subseteq> Th ` threads s" .
 
       
  1726   from this[unfolded subtree_tRAG_tG]
 
       
  1727   have " Th ` subtree (tG s) th \<subseteq> Th ` threads s" .
 
       
  1728   thus ?thesis by auto
 
  1444 qed
 
  1729 qed
 
  1445 
  1730 
  1446 end
 
  1731 end
 
  1447 
  1732 
  1448 section {* The formation of @{term RAG} *}
 
  1733 section {* The formation of @{term RAG} *}
 
  2314     interpret vt: valid_trace_set s e th prio using Set
 
  2599     interpret vt: valid_trace_set s e th prio using Set
 
  2315       by (unfold_locales, simp)
 
  2600       by (unfold_locales, simp)
 
  2316     show ?thesis using Cons by simp
 
  2601     show ?thesis using Cons by simp
 
  2317   qed
 
  2602   qed
 
  2318 qed
 
  2603 qed
 
       
  2604 
       
  2605 lemma finite_tRAG: "finite (tRAG s)"
 
       
  2606 proof -
 
       
  2607   from finite_RAG[unfolded RAG_split]
 
       
  2608   have "finite (wRAG s)" "finite (hRAG s)" by auto
 
       
  2609   from finite_relcomp[OF this] tRAG_def
 
       
  2610   show ?thesis by simp
 
       
  2611 qed
 
       
  2612 
       
  2613 lemma finite_tG: "finite (tG s)"
 
       
  2614   by (unfold tG_def, insert finite_tRAG, auto)
 
       
  2615 
  2319 end
 
  2616 end
 
  2320 
  2617 
  2321 subsection {* Uniqueness of waiting *}
 
  2618 subsection {* Uniqueness of waiting *}
 
  2322 
  2619 
  2323 text {*
 
  2620 text {*
 
  2865   show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto
 
  3162   show "wRAG s \<subseteq> RAG s" unfolding RAG_split by auto
 
  2866 next
 
  3163 next
 
  2867   show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto
 
  3164   show "hRAG s \<subseteq> RAG s" unfolding RAG_split by auto
 
  2868 qed
 
  3165 qed
 
  2869 
  3166 
       
  3167 lemma rel_map_alt_def: "rel_map f R = map_prod f f ` R"
 
       
  3168   by (unfold rel_map_def pairself_def map_prod_def, auto)
 
       
  3169 
       
  3170 lemma acyclic_tG: "acyclic (tG s)"
 
       
  3171 proof -
 
       
  3172   have "acyclic (rel_map the_thread (tRAG s))"
 
       
  3173   proof(rule rel_map_acyclic [OF acyclic_tRAG])
 
       
  3174     show "inj_on the_thread (Domain (tRAG s) \<union> Range (tRAG s))"
 
       
  3175       by (unfold tRAG_alt_def Domain_def Range_def inj_on_def, auto)
 
       
  3176   qed
 
       
  3177   thus ?thesis
 
       
  3178   by (unfold tG_def, fold rel_map_alt_def, simp)
 
       
  3179 qed
 
       
  3180 
  2870 lemma sgv_wRAG: "single_valued (wRAG s)"
 
  3181 lemma sgv_wRAG: "single_valued (wRAG s)"
 
  2871   using waiting_unique
 
  3182   using waiting_unique
 
  2872   by (unfold single_valued_def wRAG_def, auto)
 
  3183   by (unfold single_valued_def wRAG_def, auto)
 
  2873 
  3184 
  2874 lemma sgv_hRAG: "single_valued (hRAG s)"
 
  3185 lemma sgv_hRAG: "single_valued (hRAG s)"
 
  2876   by (unfold single_valued_def hRAG_def, auto)
 
  3187   by (unfold single_valued_def hRAG_def, auto)
 
  2877 
  3188 
  2878 lemma sgv_tRAG: "single_valued (tRAG s)"
 
  3189 lemma sgv_tRAG: "single_valued (tRAG s)"
 
  2879   by (unfold tRAG_def, rule single_valued_relcomp, 
  3190   by (unfold tRAG_def, rule single_valued_relcomp, 
  2880               insert sgv_wRAG sgv_hRAG, auto)
 
  3191               insert sgv_wRAG sgv_hRAG, auto)
 
       
  3192 
       
  3193 lemma sgv_tG: "single_valued (tG s)"
 
       
  3194 proof -
 
       
  3195   { fix x y z
 
       
  3196     assume h: "(x, y) \<in> tG s" "(x, z) \<in> tG s"
 
       
  3197     from tG_tRAG[OF h(1)] tG_tRAG[OF h(2)]
 
       
  3198     have "(Th x, Th y) \<in> tRAG s" "(Th x, Th z) \<in> tRAG s" by auto
 
       
  3199     from sgv_tRAG[unfolded single_valued_def, rule_format, OF this]
 
       
  3200     have "y = z" by simp
 
       
  3201   } thus ?thesis by (unfold single_valued_def, auto)
 
       
  3202 qed
 
  2881 
  3203 
  2882 end
 
  3204 end
 
  2883 
  3205 
  2884 text {*
 
  3206 text {*
 
  2885   It can be shown that @{term tRAG} is also a 
  3207   It can be shown that @{term tRAG} is also a 
  2891   from sgv_tRAG show "single_valued (tRAG s)" .
 
  3213   from sgv_tRAG show "single_valued (tRAG s)" .
 
  2892 next
 
  3214 next
 
  2893   from acyclic_tRAG show "acyclic (tRAG s)" .
 
  3215   from acyclic_tRAG show "acyclic (tRAG s)" .
 
  2894 qed
 
  3216 qed
 
  2895 
  3217 
       
  3218 sublocale valid_trace < forest_s_tG?: forest "tG s"
 
       
  3219 proof(unfold_locales)
 
       
  3220   from sgv_tG show "single_valued (tG s)" .
 
       
  3221 next
 
       
  3222   from acyclic_tG show "acyclic (tG s)" .
 
       
  3223 qed
 
       
  3224 
       
  3225 context valid_trace
 
       
  3226 begin
 
       
  3227 
       
  3228 lemma wf_tRAG: "wf (tRAG s)"
 
       
  3229 proof(rule wf_subset)
 
       
  3230       show "wf (RAG s O RAG s)" using wf_RAG
 
       
  3231         by (fold wf_comp_self, simp)
 
       
  3232 next
 
       
  3233       show "tRAG s \<subseteq> (RAG s O RAG s)"
 
       
  3234         by (unfold tRAG_alt_def, auto)
 
       
  3235 qed
 
       
  3236 
       
  3237 lemma wf_tG: "wf (tG s)"
 
       
  3238 proof(rule finite_acyclic_wf)
 
       
  3239   from finite_tG show "finite (tG s)" .
 
       
  3240 next
 
       
  3241   from acyclic_tG show "acyclic (tG s)" .
 
       
  3242 qed
 
       
  3243 
       
  3244 lemma finite_children_tRAG: "finite (children (tRAG s) x)"
 
       
  3245   proof(unfold tRAG_def, rule fbranch_compose1[rule_format])
 
       
  3246     fix x show "finite (children (wRAG s) x)" 
       
  3247     proof(rule finite_fbranchI1[rule_format])
 
       
  3248       show "finite (wRAG s)" using finite_RAG[unfolded RAG_split] by auto
 
       
  3249     qed
 
       
  3250   next
 
       
  3251     fix x
 
       
  3252     show "finite (children (hRAG s) x)"
 
       
  3253     proof(rule finite_fbranchI1[rule_format])
 
       
  3254       show "finite (hRAG s)" using finite_RAG[unfolded RAG_split] by auto
 
       
  3255     qed
 
       
  3256   qed
 
       
  3257 
       
  3258 lemma children_map_prod: 
       
  3259   assumes "inj f"
 
       
  3260   shows " children (map_prod f f ` r) (f x) = f ` (children r x)" (is "?L = ?R")
 
       
  3261 proof -
 
       
  3262   { fix e
 
       
  3263     assume "e \<in> ?L"
 
       
  3264     then obtain e' x' where h: "e = f e'" "f x' = f x" "(e', x') \<in> r"
 
       
  3265       by (auto simp:children_def)
 
       
  3266     with assms[unfolded inj_on_def, rule_format]
 
       
  3267     have eq_x': "x' = x" by auto
 
       
  3268     with h
 
       
  3269     have "e \<in> ?R" by  (unfold children_def, auto)
 
       
  3270   } moreover {
 
       
  3271     fix e
 
       
  3272     assume "e \<in> ?R"
 
       
  3273     hence "e \<in> ?L" by (auto simp:children_def)
 
       
  3274   } ultimately show ?thesis by auto
 
       
  3275 qed
 
       
  3276 
       
  3277 lemma finite_children_tG: "finite (children (tG s) x)"
 
       
  3278 proof -
 
       
  3279   have "(children (tRAG s) (Th x)) = Th ` children (tG s) x"
 
       
  3280     by (unfold tRAG_def_tG, subst children_map_prod, auto simp:inj_on_def)
 
       
  3281   from finite_children_tRAG[of "Th x", unfolded this]
 
       
  3282   have "finite (Th ` children (tG s) x)" .
 
       
  3283   from finite_imageD[OF this]
 
       
  3284   show ?thesis by (auto simp:inj_on_def)
 
       
  3285 qed
 
       
  3286 
       
  3287 end
 
  2896 
  3288 
  2897 sublocale valid_trace < fsbttRAGs?: fforest "tRAG s"
 
  3289 sublocale valid_trace < fsbttRAGs?: fforest "tRAG s"
 
  2898 proof
 
  3290 proof
 
  2899   fix x
 
  3291   fix x
 
  2900   show "finite (children (tRAG s) x)"
 
  3292   show "finite (children (tRAG s) x)"
 
  2917         by (fold wf_comp_self, simp)
 
  3309         by (fold wf_comp_self, simp)
 
  2918   next
 
  3310   next
 
  2919       show "tRAG s \<subseteq> (RAG s O RAG s)"
 
  3311       show "tRAG s \<subseteq> (RAG s O RAG s)"
 
  2920         by (unfold tRAG_alt_def, auto)
 
  3312         by (unfold tRAG_alt_def, auto)
 
  2921   qed
 
  3313   qed
 
       
  3314 qed
 
       
  3315 
       
  3316 sublocale valid_trace < fsbttGs?: fforest "tG s"
 
       
  3317 proof
 
       
  3318   fix x
 
       
  3319   show "finite (children (tG s) x)" 
       
  3320     by (simp add:finite_children_tG)
 
       
  3321 next
 
       
  3322   show "wf (tG s)" by (simp add:wf_tG)
 
  2922 qed
 
  3323 qed
 
  2923 
  3324 
  2924 section {* Chain to readys *}
 
  3325 section {* Chain to readys *}
 
  2925 
  3326 
  2926 text {*
 
  3327 text {*
 
  3002  Domain_def)
 
  3403  Domain_def)
 
  3003   from chain_building [rule_format, OF this]
 
  3404   from chain_building [rule_format, OF this]
 
  3004   show ?thesis by auto
 
  3405   show ?thesis by auto
 
  3005 qed
 
  3406 qed
 
  3006 
  3407 
       
  3408 lemma th_chain_to_ready_tG:
 
       
  3409   assumes th_in: "th \<in> threads s"
 
       
  3410   shows "th \<in> readys s \<or> (\<exists> th'. th' \<in> readys s \<and> (th, th') \<in> (tG s)^+)"
 
       
  3411 proof -
 
       
  3412   from th_chain_to_ready[OF assms]
 
       
  3413   show ?thesis
 
       
  3414   using dependants_alt_def1 dependants_alt_tG by blast 
       
  3415 qed
 
       
  3416 
  3007 text {*
 
  3417 text {*
 
  3008   The following lemma is a technical one to show 
  3418   The following lemma is a technical one to show 
  3009   that the set of threads in the subtree of any thread
 
  3419   that the set of threads in the subtree of any thread
 
  3010   is finite.
 
  3420   is finite.
 
  3011 *}
 
  3421 *}
 
  3024      ultimately show ?thesis by auto
 
  3434      ultimately show ?thesis by auto
 
  3025   qed
 
  3435   qed
 
  3026   ultimately show ?thesis by auto
 
  3436   ultimately show ?thesis by auto
 
  3027 qed
 
  3437 qed
 
  3028 
  3438 
       
  3439 (* ccc *)
 
       
  3440 
       
  3441 lemma readys_no_tRAG_chain:
 
       
  3442   assumes "th1 \<in> readys s"
 
       
  3443   and "th2 \<in> readys s"
 
       
  3444   and "th1 \<noteq> th2"
 
       
  3445   shows "(Th th1, Th th2) \<notin> (tRAG s)^*"
 
       
  3446 proof
 
       
  3447   assume "(Th th1, Th th2) \<in> (tRAG s)\<^sup>*"
 
       
  3448   from rtranclD[OF this]
 
       
  3449   show False
 
       
  3450   proof
 
       
  3451     assume "Th th1 = Th th2" with assms show ?thesis by simp
 
       
  3452   next
 
       
  3453     assume "Th th1 \<noteq> Th th2 \<and> (Th th1, Th th2) \<in> (tRAG s)\<^sup>+"
 
       
  3454     hence "(Th th1, Th th2) \<in> (tRAG s)\<^sup>+" by auto
 
       
  3455     from tranclD[OF this] obtain cs where "(Th th1, Cs cs) \<in> RAG s"
 
       
  3456       by (unfold tRAG_alt_def, auto)
 
       
  3457     from in_RAG_E[OF this] have "th1 \<notin> readys s" by (unfold readys_def, auto)
 
       
  3458     with assms show ?thesis by simp
 
       
  3459   qed
 
       
  3460 qed
 
       
  3461 
       
  3462 lemma readys_indep:
 
       
  3463   assumes "th1 \<in> readys s"
 
       
  3464   and "th2 \<in> readys s"
 
       
  3465   and "th1 \<noteq> th2"
 
       
  3466   shows "indep (tRAG s) (Th th1) (Th th2)"
 
       
  3467   using assms readys_no_tRAG_chain
 
       
  3468   unfolding indep_def by blast
 
       
  3469 
       
  3470 lemma readys_indep_tG:
 
       
  3471   assumes "th1 \<in> readys s"
 
       
  3472   and "th2 \<in> readys s"
 
       
  3473   and "th1 \<noteq> th2"
 
       
  3474   shows "indep (tG s) th1 th2"
 
       
  3475   using assms
 
       
  3476   unfolding indep_def
 
       
  3477   using readys_no_tRAG_chain rtrancl_tG_tRAG by blast
 
       
  3478 
       
  3479 text {*
 
       
  3480   The following lemma @{text "thread_chain"} holds on any living thread, 
       
  3481   not necessarily a running one. 
       
  3482 *}
 
       
  3483 lemma thread_chain:
 
       
  3484   assumes "th \<in> threads s"
 
       
  3485   obtains th' where "th' \<in> subtree (tG s) th" "th' \<in> threads s"
 
       
  3486                     "the_preced s th' = Max (the_preced s ` subtree (tG s) th)"
 
       
  3487 proof -
 
       
  3488   have "Max (the_preced s ` subtree (tG s) th) \<in> the_preced s ` subtree (tG s) th"
 
       
  3489   proof(rule Max_in)
 
       
  3490     show "finite (the_preced s ` subtree (tG s) th)" 
       
  3491         by (simp add: fsbttGs.finite_subtree)
 
       
  3492   next
 
       
  3493     show "the_preced s ` subtree (tG s) th \<noteq> {}" using subtree_def by fastforce 
       
  3494   qed
 
       
  3495   then obtain th' where 
       
  3496        h: "th' \<in> subtree (tG s) th"
 
       
  3497                     "the_preced s th' = Max (the_preced s ` subtree (tG s) th)"
 
       
  3498   by auto
 
       
  3499   moreover have "th' \<in> threads s"
 
       
  3500   proof -
 
       
  3501     from assms have "th \<in> threads s" .
 
       
  3502     from subtree_tG_thread[OF this] and h 
       
  3503     show ?thesis by auto
 
       
  3504   qed
 
       
  3505   ultimately show ?thesis using that by auto
 
       
  3506 qed
 
       
  3507 
  3029 text {*
 
  3508 text {*
 
  3030   The following two lemmas shows there is at most one running thread 
  3509   The following two lemmas shows there is at most one running thread 
  3031   in the system.
 
  3510   in the system.
 
  3032 *}
 
  3511 *}
 
  3033 lemma running_unique:
 
  3512 lemma running_unique:
 
       
  3513   assumes running_1: "th1 \<in> running s"
 
       
  3514   and running_2: "th2 \<in> running s"
 
       
  3515   shows "th1 = th2"
 
       
  3516 proof -
 
       
  3517   -- {* According to lemma @{thm thread_chain}, 
       
  3518         each living threads is chained to a thread in its subtree, and this
 
       
  3519         target thread holds the highest precedence of the subtree.
 
       
  3520 
       
  3521         The chains for @{term th1} and @{term th2} are established 
       
  3522         first in the following in @{text "h1"} and @{text "h2"}:
 
       
  3523      *}
 
       
  3524   have "th1 \<in> threads s" using assms
 
       
  3525     by (unfold running_def readys_def, auto)
 
       
  3526   from thread_chain[OF this]
 
       
  3527   obtain th1' where 
       
  3528       h1: "th1' \<in> subtree (tG s) th1" 
       
  3529           "the_preced s th1' = Max (the_preced s ` subtree (tG s) th1)"
 
       
  3530           "th1' \<in> threads s"
 
       
  3531       by auto
 
       
  3532   have "th2 \<in> threads s" using assms
 
       
  3533     by (unfold running_def readys_def, auto)
 
       
  3534   from thread_chain[OF this]
 
       
  3535   obtain th2' where 
       
  3536       h2: "th2' \<in> subtree (tG s) th2" 
       
  3537           "the_preced s th2' = Max (the_preced s ` subtree (tG s) th2)"
 
       
  3538           "th2' \<in> threads s"
 
       
  3539       by auto
 
       
  3540   -- {* It can be proved that the chained thread for @{term th1} and @{term th2}
 
       
  3541         must be equal:
 
       
  3542      *}
 
       
  3543   have eq_th': "th1' = th2'"
 
       
  3544   proof -
 
       
  3545     have "the_preced s th1' = the_preced s th2'" 
       
  3546     proof -
 
       
  3547       from running_1 and running_2 have "cp s th1 = cp s th2"
 
       
  3548           unfolding running_def by auto
 
       
  3549       from this[unfolded cp_alt_def2]
 
       
  3550       have eq_max: "Max (the_preced s ` subtree (tG s) th1) = 
       
  3551                     Max (the_preced s ` subtree (tG s) th2)" .
 
       
  3552       with h1(2) h2(2)
 
       
  3553       show ?thesis by metis
 
       
  3554     qed
 
       
  3555     from preced_unique[OF this[unfolded the_preced_def] h1(3) h2(3)]
 
       
  3556     show ?thesis .
 
       
  3557   qed
 
       
  3558   -- {* From this, it can be derived that the two sub-trees 
       
  3559         rooted by @{term th1} and @{term th2} must overlap: *}
 
       
  3560   have overlapping: "th1' \<in> subtree (tG s) th1 \<inter> subtree (tG s) th2" 
       
  3561      using  eq_th' h1(1) h2(1) by auto
 
       
  3562   -- {* However, this would be in contradiction with the fact
 
       
  3563         that two independent sub-trees can not overlap, 
       
  3564         if @{term "th1 \<noteq> th2"} (therefore, each roots an independent sub-trees).
 
       
  3565         Therefore, @{term th1} and @{term th2} must be equal.
 
       
  3566      *}
 
       
  3567   { assume neq: "th1 \<noteq> th2"
 
       
  3568     -- {* According to @{thm readys_indep_tG}, two different threads 
       
  3569           in ready queue must be independent with each other: *}
 
       
  3570     have "indep (tG s) th1 th2"
 
       
  3571       by (rule readys_indep_tG[OF _ _ neq], insert assms, auto simp:running_def)
 
       
  3572     -- {* Therefore, according to lemma @{thm subtree_disjoint},
 
       
  3573           the two sub-trees rooted by them can not overlap: 
       
  3574     *}
 
       
  3575     from subtree_disjoint[OF this]
 
       
  3576     have "subtree (tG s) th1 \<inter> subtree (tG s) th2 = {}" .
 
       
  3577     -- {* In contradiction with @{thm overlapping}: *}
 
       
  3578     with overlapping have False by auto
 
       
  3579   } thus ?thesis by auto
 
       
  3580 qed
 
       
  3581 
       
  3582 text {*
 
       
  3583   The following two lemmas shows there is at most one running thread 
       
  3584   in the system.
 
       
  3585 *}
 
       
  3586 lemma running_unique_old:
 
  3034   assumes running_1: "th1 \<in> running s"
 
  3587   assumes running_1: "th1 \<in> running s"
 
  3035   and running_2: "th2 \<in> running s"
 
  3588   and running_2: "th2 \<in> running s"
 
  3036   shows "th1 = th2"
 
  3589   shows "th1 = th2"
 
  3037 proof -
 
  3590 proof -
 
  3038   from running_1 and running_2 have "cp s th1 = cp s th2"
 
  3591   from running_1 and running_2 have "cp s th1 = cp s th2"
 
  5110     shows "e = Exit th"
 
  5663     shows "e = Exit th"
 
  5111     using assms
 
  5664     using assms
 
  5112     by (cases e, auto)
 
  5665     by (cases e, auto)
 
  5113 
  5666 
  5114 end
 
  5667 end
 
       
  5668
pip